coe_inf — Mathlib

English

The submodule underlying the infimum of a set S of Lie subalgebras equals the infimum of the corresponding submodules.

Русский

Подмодуль, лежащий под инфимумом множества S подалгебр, равен инфимуму соответствующих подмодулей.

LaTeX

$$$ (sInf S).toSubmodule = sInf (\\{ (s : Submodule R L) \\mid s \\in S \\}) $$$

Lean4

@[simp]
theorem coe_inf : (↑(K ⊓ K') : Set L) = (K : Set L) ∩ (K' : Set L) :=
  rfl

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