comap_sup_eq — Mathlib

English

If H ≤ L and K ≤ L, then H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L.

Русский

Если H ≤ L и K ≤ L, то H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L.

LaTeX

$$$H \\le L,\\; K \\le L \\Rightarrow H . subgroupOf L \\;\\sqcup\\; K . subgroupOf L = (H \\sqcup K) . subgroupOf L$$$

Lean4

@[to_additive]
theorem comap_sup_eq (H K : Subgroup N) (hf : Function.Surjective f) : comap f H ⊔ comap f K = comap f (H ⊔ K) :=
  comap_sup_eq_of_le_range f (range_eq_top.2 hf ▸ le_top) (range_eq_top.2 hf ▸ le_top)

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