map_iInf — Mathlib

English

If s is a family of intermediate fields indexed by ι, then the image of their infimum equals the infimum of their images: (iInf s).map f = ⨅ i, (s i).map f.

Русский

Образ пересечения по индексу равен пересечению образов: (iInf s).map f = ⨅ i, (s i).map f.

LaTeX

$$$\operatorname{map} f (\bigwedge_i s_i) = \bigwedge_i \operatorname{map} f (s_i)$$$

Lean4

theorem map_iInf {ι : Sort*} [Nonempty ι] (f : E →ₐ[F] K) (s : ι → IntermediateField F E) :
    (iInf s).map f = ⨅ i, (s i).map f := by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coe ∘ s)

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