instInfOpenSubgroup — Mathlib

English

The infimum (meet) of two open subgroups U and V in OpenSubgroup G is their intersection, and the underlying set is U ∩ V.

Русский

Наименьшее значение двух открытых подгрупп U и V в OpenSubgroup G равно их пересечению, а множество подгруппы равно U ∩ V.

LaTeX

$$$$ U \\wedge V = U \\cap V. $$$$

Lean4

@[to_additive]
instance instInfOpenSubgroup : Min (OpenSubgroup G) :=
  ⟨fun U V ↦ ⟨U ⊓ V, U.isOpen.inter V.isOpen⟩⟩

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