sInf_glb — Mathlib

English

In the lattice of Lie subalgebras, the infimum sInf S is a greatest lower bound of S.

Русский

В решётке подалгебр Ли инфимум sInf S является наибольшим нижним пределом множества S.

LaTeX

$$$ IsGLB\\, S\\, (sInf S)$$$

Lean4

theorem sInf_glb (S : Set (LieSubalgebra R L)) : IsGLB S (sInf S) :=
  by
  have h : ∀ K K' : LieSubalgebra R L, (K : Set L) ≤ K' ↔ K ≤ K' :=
    by
    intros
    exact Iff.rfl
  apply IsGLB.of_image @h
  simp only [coe_sInf]
  exact isGLB_biInf

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