second_iso_of_eq — Mathlib

English

Given x,y,a,b with IsMaximal x a and a ⊔ relationships, there is an isomorphism between (x,a) and (b,y).

Русский

При условии IsMaximal x a и соответствующей связи между a и y существует изоморфизм между парами (x,a) и (b,y).

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\ X] [\\mathrm{JordanHolderLattice}\ X],\\ IsMaximal\\ x\\ a \\to\\ Eq (\\mathrm SemilatticeSup.toMax.max x y) a \\to Eq (\\mathrm SemilatticeInf.toMin.min x y) b \\to Iso (x,a) (b,y).$$$

Lean4

theorem second_iso_of_eq {x y a b : X} (hm : IsMaximal x a) (ha : x ⊔ y = a) (hb : x ⊓ y = b) : Iso (x, a) (b, y) := by
  substs a b; exact second_iso hm

Похожие утверждения