coe_iInf — Mathlib

English

Let {N_i} be a family of Lie submodules of a Lie module M. Then the underlying set of their infimum is the intersection of their underlying sets.

Русский

Пусть {N_i} — семейство Ли-подмодулей модуля M. Тогда множество, лежащее в инфимума, равно пересечению множеств N_i.

LaTeX

$$$\left(\inf_i N_i\right)^{\text{set}} = \bigcap_i N_i^{\text{set}}$$$

Lean4

@[simp]
theorem coe_iInf {ι} (p : ι → LieSubmodule R L M) : (↑(⨅ i, p i) : Set M) = ⋂ i, ↑(p i) := by rw [iInf, coe_sInf];
  simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']

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