X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
hb : x ⊔ y = b
⊢ IsMaximal a y
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
⊢ IsMaximal a y
have hb : x ⊔ y = b := sup_eq_of_isMaximal hxb hyb hxy
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxy : x ≠ y
hxb : IsMaximal x (x ⊔ y)
hyb : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
hb : x ⊔ y = b
⊢ IsMaximal a y
substs a b
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxy : x ≠ y
hxb : IsMaximal x (x ⊔ y)
hyb : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y
exact isMaximal_inf_right_of_isMaximal_sup hxb hyb