sInf_toSubfield — Mathlib

English

The infimum of a set of intermediate fields, when viewed as a subfield, equals the infimum of their images as subfields.

Русский

Инфинум множества промежуточных полей, как подполья, равен инфимума их изображений как подполья.

LaTeX

$$$ (sInf S).toSubfield = sInf (toSubfield '' S) $$$

Lean4

@[simp]
theorem sInf_toSubfield (S : Set (IntermediateField F E)) : (sInf S).toSubfield = sInf (toSubfield '' S) :=
  SetLike.coe_injective <| by simp

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