coe_sInf — Mathlib

English

The carrier of the infimum sInf S of a set S of subfields equals the intersection over S of their carriers: (sInf S : Set K) = ⋂ p ∈ S, (p : Set K).

Русский

Носитель наименьшего элемента множества подполей sInf S равен пересечению носителей элементов S: (sInf S : Set K) = ⋂ p ∈ S, (p : Set K).

LaTeX

$$$(sInf S : Set K) = \bigcap_{p \in S} (p : Set K)$$$

Lean4

@[simp, norm_cast]
theorem coe_sInf (S : Set (Subfield K)) : ((sInf S : Subfield K) : Set K) = ⋂ s ∈ S, ↑s :=
  show ((sInf (Subfield.toSubring '' S) : Subring K) : Set K) = ⋂ s ∈ S, ↑s by simp

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