sInf_toSubring — Mathlib

English

The infimum sInf S of a set S of subfields, viewed as a subring, equals the infimum of the corresponding Subring objects: (sInf S).toSubring = ⨅ t ∈ S, Subfield.toSubring t.

Русский

Наименьшее нижнее ограничение множества подполей S, рассмотренное как подкольцо, равно наименьшему нижнему ограничению множества t.toSubring, где t пробирает S.

LaTeX

$$$\,(sInf\, S).toSubring = \bigsqcap_{t \in S} (t.toSubring)$$$

Lean4

@[simp]
theorem sInf_toSubring (s : Set (Subfield K)) : (sInf s).toSubring = ⨅ t ∈ s, Subfield.toSubring t :=
  by
  ext x
  simp [mem_sInf, ← sInf_image, Subring.mem_sInf]

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