map_iInf — Mathlib

English

The equality of the indexed coe is given by set-theoretic intersection of the indexed subalgebras.

Русский

Равенство индексации коe задаётся пересечением по индексам.

LaTeX

$$$ (iInf i, S_i).coe = \\bigcap_i S_i.coe $$$

Lean4

theorem map_iInf {ι : Sort*} [Nonempty ι] [IsScalarTower R B B] [SMulCommClass R B B] (f : F)
    (hf : Function.Injective f) (S : ι → NonUnitalSubalgebra R A) :
    ((⨅ i, S i).map f : NonUnitalSubalgebra 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)

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