map_le_iff_le_comap — Mathlib

English

For LieHom f and LieIdeals I ⊆ L, J ⊆ L', we have map f I ≤ J if and only if I ≤ comap f J.

Русский

Для гомоморфизма Ли f и Ли-идеалов I ⊆ L, J ⊆ L' верно: map f I ≤ J тогда и только тогда, когда I ≤ comap f J.

LaTeX

$$$\\text{map}(f,I) ≤ J \\;\\iff \\; I ≤ \\mathrm{comap}(f,J)$$$

Lean4

theorem map_le_iff_le_comap : map f I ≤ J ↔ I ≤ comap f J :=
  by
  rw [map_le]
  exact Set.image_subset_iff

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