mem_inf — Mathlib

English

The underlying set of the infimum of a set of Lie subalgebras is the intersection of the underlying sets of those subalgebras.

Русский

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

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 mem_inf (x : L) : x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K' := by
  rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule, Submodule.mem_inf]

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