map_le — Mathlib

English

The image S under f is contained in U if and only if S is contained in the preimage of U under f.

Русский

Образ S по f содержится в U тогда и только тогда, когда S содержится в предобразе U по f.

LaTeX

$$map f S \le U \iff S \le comap f U.$$

Lean4

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

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