coe_sInf — Mathlib

English

The underlying set of the infimum of a set of Lie subalgebras equals the intersection of their underlying sets.

Русский

Множество инфимума множества подалгебр равно пересечению соответствующих множеств.

LaTeX

$$$ (sInf S).toSubmodule = Submodule.instInfSet.sInf (setOf fun x => Exists fun s => And (Set.instMembership.mem S s) (Eq s.toSubmodule x))$$$

Lean4

@[simp]
theorem coe_sInf (S : Set (LieSubalgebra R L)) : (↑(sInf S) : Set L) = ⋂ s ∈ S, (s : Set L) :=
  by
  rw [← coe_toSubmodule, sInf_toSubmodule, Submodule.coe_sInf]
  ext x
  simp

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