instMax — Mathlib

English

The collection of open subgroups of a topological group G is equipped with a maximum operation: for any two open subgroups U and V, their join U ⊔ V is again an open subgroup of G.

Русский

Множество открытых подпгруп G наделено операцией максимума: для любых открытых подгрупп U и V их сумма U ⊔ V вновь является открытой подгруппой G.

LaTeX

$$$U \\vee V \\text{ is an open subgroup of } G$$$

Lean4

@[to_additive]
instance : Max (OpenSubgroup G) :=
  ⟨fun U V ↦ ⟨U ⊔ V, Subgroup.isOpen_mono (le_sup_left : U.1 ≤ U.1 ⊔ V.1) U.isOpen⟩⟩

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