comap_mono — Mathlib

English

If S1 ≤ S2 are StarSubalgebras of B, then their preimages under a fixed f satisfy S1.comap f ≤ S2.comap f.

Русский

Если S1 ≤ S2 — звездные подсалгебры B, то их прообраз под фиксированным f удовлетворяет S1.comap f ≤ S2.comap f.

LaTeX

$$$S_1 \\le S_2 \\Rightarrow S_1{}.comap\\ f \\le S_2{}.comap\\ f$$$

Lean4

theorem comap_mono {S₁ S₂ : StarSubalgebra R B} {f : A →⋆ₐ[R] B} : S₁ ≤ S₂ → S₁.comap f ≤ S₂.comap f :=
  Set.preimage_mono

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