map_comap_eq — Mathlib

English

For any f: A →ₐ[R] B and subalgebra S of B, the map of comap equals the infimum of S and the range of f.

Русский

Для любого f: A →ₐ[R] B и подпалгебры S B отображение map от comap f равно пересечению S и образам f.

LaTeX

$$$ \\mathrm{map\_comap\_eq} (f) (S) : (S.comap f).map f = S \\; \\inf \\; f.range $$$

Lean4

theorem map_comap_eq (f : A →ₐ[R] B) (S : Subalgebra R B) : (S.comap f).map f = S ⊓ f.range :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

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