isMaximal_inf_right_of_isMaximal_sup

English

In a Jordan-Hölder lattice, if x and y are maximal relative to b inside x ⊔ y, then x ⊓ y is maximal relative to y inside x ⊓ y ⊔ ? (precise formulation: given x ⊔ y with maximalities, the infimum inherits a maximality property).

Русский

В решётке Джордана–Холдера если x и y максимальны внутри x ⊔ y относительно b, то x ⊓ y имеет соответствующую максимальность по отношению к y.

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\ X] [\\mathrm{JordanHolderLattice}\ X],\\ {x\\, y : X},\\ IsMaximal\\ x\\ (x \\vee y) \\to IsMaximal\\ y\\ (x \\vee y) \\to IsMaximal\\ (x \\wedge y)\\ y.$$$

Lean4

theorem isMaximal_inf_right_of_isMaximal_sup {x y : X} (hxz : IsMaximal x (x ⊔ y)) (hyz : IsMaximal y (x ⊔ y)) :
    IsMaximal (x ⊓ y) y := by
  rw [inf_comm]
  rw [sup_comm] at hxz hyz
  exact isMaximal_inf_left_of_isMaximal_sup hyz hxz

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