map_le_iff_le_comap — Mathlib

English

For S ⊆ A, U ⊆ B, with a star-algebra homomorphism f, the order relation respects image and preimage: map f S ≤ U iff S ≤ comap f U.

Русский

Для подалгебр S ⊆ A, U ⊆ B существует отношение, что образ S через f лежит в U тогда и только тогда S лежит в предобразе U через f.

LaTeX

$$$\\mathrm{map}\ f\\ S \\le U \\iff S \\le \\mathrm{comap}\ f\\ U$$$

Lean4

theorem map_le_iff_le_comap {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} {U : StarSubalgebra R B} :
    map f S ≤ U ↔ S ≤ comap f U :=
  Set.image_subset_iff

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