comap_sup_eq_of_le_range — Mathlib

English

If H,K ≤ f.range, then comap f H ⊔ comap f K = comap f (H ⊔ K).

Русский

Если H,K ≤ f.range, тогда comap f H ⊔ comap f K = comap f (H ⊔ K).

LaTeX

$$$H,K \\le f.range \\Rightarrow comap f H \\sqcup comap f K = comap f (H \\sqcup K)$$$

Lean4

@[to_additive]
theorem comap_sup_eq_of_le_range {H K : Subgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) :
    comap f H ⊔ comap f K = comap f (H ⊔ K) :=
  map_injective_of_ker_le f ((ker_le_comap f H).trans le_sup_left) (ker_le_comap f (H ⊔ K))
    (by
      rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH, inf_eq_right.mpr hK,
        inf_eq_right.mpr (sup_le hH hK)])

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