coe_sInf — Mathlib

English

The iInf of a family of LieSubmodules maps to Submodule as the infimum of their images in Submodule.

Русский

iInf семейства LieSubmodule отображается в Submodule как инфимум их изображений в Submodule.

LaTeX

$$$ (\,\iInf i\, p i).toSubmodule = \iInf i (p i : Submodule R L) $$$

Lean4

@[simp]
theorem coe_sInf (S : Set (LieSubmodule R L M)) : (↑(sInf S) : Set M) = ⋂ s ∈ S, (s : Set M) :=
  by
  rw [← LieSubmodule.coe_toSubmodule, sInf_toSubmodule, Submodule.coe_sInf]
  ext m
  simp only [mem_iInter, mem_setOf_eq, forall_apply_eq_imp_iff₂, exists_imp, and_imp, SetLike.mem_coe, mem_toSubmodule]

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