isModularLattice_iff_inf_sup_inf_assoc

English

Equivalent characterization of modular lattices via the lt-structure with exact sequence data; equivalence expresses WellFoundedLT by an explicit simp lemma.

Русский

Эквивалентная характеристика модульных решёток через структуру LT с данными точной последовательности; эквивалентность выражается через простое лемм.

LaTeX

$$$(\text{IsModularLattice }\alpha) \iff (\forall x,y,z,\ x\wedge z\vee y\wedge z=(x\wedge z\vee y)\wedge z)$.$$

Lean4

theorem isModularLattice_iff_inf_sup_inf_assoc [Lattice α] :
    IsModularLattice α ↔ ∀ x y z : α, x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z :=
  ⟨fun h => @IsModularLattice.inf_sup_inf_assoc _ _ h, fun h => ⟨fun y z xz => by rw [← inf_eq_left.2 xz, h]⟩⟩

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