iso_refl — Mathlib

English

If x is maximal over y, then the canonical isomorphism between (x,y) and itself exists (reflexivity of the isomorphism).

Русский

Если x максимален над y, то существует тождественный изоморфизм между (x,y) и (x,y).

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\ X] [\\mathrm{JordanHolderLattice}\ X],\\ IsMaximal\\ x\\ y \\to\\ Iso\\ { fst := x, snd := y } { fst := x, snd := y }.$$$

Lean4

theorem iso_refl {x y : X} (h : IsMaximal x y) : Iso (x, y) (x, y) :=
  second_iso_of_eq h (sup_eq_right.2 (le_of_lt (lt_of_isMaximal h))) (inf_eq_left.2 (le_of_lt (lt_of_isMaximal h)))

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