map_iInf — Mathlib

English

With an injective star-algebra homomorphism f, map f preserves iInf: map f (iInf s) = iInf (map f ∘ s).

Русский

При инъективном отображении f отображение iInf сохраняется: map f (iInf s) = iInf (map f ∘ s).

LaTeX

$$$\operatorname{map} f (\mathrm{iInf}\; s) = \mathrm{iInf}\; (\lambda i. \operatorname{map} f (s i))$$$

Lean4

theorem map_iInf {ι : Sort*} [Nonempty ι] (f : A →⋆ₐ[R] B) (hf : Function.Injective f) (s : ι → StarSubalgebra R A) :
    map f (iInf s) = ⨅ (i : ι), map f (s i) :=
  by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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