sInf_toSubalgebra — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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