le_comap_mul — Mathlib

English

The comaps distribute over multiplication: comap f K * comap f L ≤ comap f (K * L).

Русский

Образы через comap распространяются на умножение: comap f K * comap f L ≤ comap f (K * L).

LaTeX

$$comap f K * comap f L ≤ comap f (K * L)$$

Lean4

theorem le_comap_mul : comap f K * comap f L ≤ comap f (K * L) :=
  map_le_iff_le_comap.1 <|
    (Ideal.map_mul f (comap f K) (comap f L)).symm ▸
      mul_mono (map_le_iff_le_comap.2 <| le_rfl) (map_le_iff_le_comap.2 <| le_rfl)

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