coe_iInf — Mathlib

English

The underlying set of the infimum over an indexed family of submonoids equals the intersection of the underlying sets of the indexed submonoids.

Русский

Множество подмножества: основание инфимума по индексу совпадает с пересечением оснований соответствующих подпmonoid.

LaTeX

$$↑(⨅ i, S i) = ⋂ i, ↑(S i)$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_iInf {ι : Sort*} {S : ι → Submonoid M} : (↑(⨅ i, S i) : Set M) = ⋂ i, S i := by
  simp only [iInf, coe_sInf, Set.biInter_range]

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