map_iInf — Mathlib

English

Reiterates that the map of an infimum across a family equals the infimum of the mapped family: (⨅ i, S_i).map f = ⨅ i, (S_i).map f.

Русский

Ещё раз: отображение пересечения сохраняется по компонентам: (⨅ i, S_i).map f = ⨅ i, (S_i).map f.

LaTeX

$$$((\\iInf_i S_i).map f) = \\iInf_i (S_i.map f)$$$

Lean4

theorem map_iInf {ι : Sort*} [Nonempty ι] [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F)
    (hf : Function.Injective f) (S : ι → NonUnitalStarSubalgebra R A) :
    ((⨅ i, S i).map f : NonUnitalStarSubalgebra R B) = ⨅ i, (S i).map f :=
  by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ S)

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