sup_subgroupOf_eq — Mathlib

English

Equivalent form of the previous equality in terms of semiformal lattice language.

Русский

Эквивалентная форма предыдущего равенства в терминах полупрямой решетки.

LaTeX

$$Eq (SemilatticeInf.toPartialOrder.max (H.subgroupOf L) (K.subgroupOf L)) ((H ⊔ K).subgroupOf L)$$

Lean4

@[to_additive]
theorem sup_subgroupOf_eq {H K L : Subgroup G} (hH : H ≤ L) (hK : K ≤ L) :
    H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L :=
  comap_sup_eq_of_le_range L.subtype (hH.trans_eq L.range_subtype.symm) (hK.trans_eq L.range_subtype.symm)

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