map_le — Mathlib

English

Let f: A → B be a homomorphism and S ⊆ A, U ⊆ B be nonunital subalgebras. Then the image f[S] is contained in U if and only if S is contained in the preimage comap f[U], i.e., f[S] ⊆ U ⇔ S ⊆ f^{-1}(U).

Русский

Пусть f: A → B — гомоморфизм, S ⊆ A и U ⊆ B — немоноидальные подалгебры. Тогда образ f[S] содержится в U тогда и только тогда S содержится в предобразе f^{-1}(U).

LaTeX

$$$f[S] \\subseteq U \\;\\Longleftrightarrow\\; S \\subseteq f^{-1}[U]$$$

Lean4

theorem map_le {S : NonUnitalSubalgebra R A} {f : F} {U : NonUnitalSubalgebra R B} : map f S ≤ U ↔ S ≤ comap f U :=
  Set.image_subset_iff

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