English
If x ⊔ y = a and x ⊓ y = b with IsMaximal x a and IsMaximal y b, then there is an isomorphism between the pairs (x,a) and (b,y).
Русский
При x ⊔ y = a и x ⊓ y = b и при этом x максимально относительно a и y максимально относительно b существует изоморфизм между парами (x,a) и (b,y).
LaTeX
$$$\\forall {X} [\\mathrm{Lattice}\ X] [\\mathrm{JordanHolderLattice}\ X],\\\\ {x\\, y\\, a\\, b : X},\\ IsMaximal\\ x\\ a \\to x \\vee y = a \\to x \\wedge y = b \\to Iso\\ { fst := x, snd := a } { fst := b, snd := y }.$$$
Lean4
theorem isMaximal_of_eq_inf (x b : X) {a y : X} (ha : x ⊓ y = a) (hxy : x ≠ y) (hxb : IsMaximal x b)
(hyb : IsMaximal y b) : IsMaximal a y :=
by
have hb : x ⊔ y = b := sup_eq_of_isMaximal hxb hyb hxy
substs a b
exact isMaximal_inf_right_of_isMaximal_sup hxb hyb
