instSemilatticeInfOpenSubgroup — Mathlib

English

OpenSubgroup G has a meet (infimum) operation given by intersection: inf(U,V) = U ∩ V.

Русский

У OpenSubgroup G существует операция meet (infimum), которая задаётся пересечением: inf(U,V) = U ∩ V.

LaTeX

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

Lean4

@[to_additive]
instance instSemilatticeInfOpenSubgroup : SemilatticeInf (OpenSubgroup G) :=
  { SetLike.coe_injective.semilatticeInf ((↑) : OpenSubgroup G → Set G) fun _ _ ↦ rfl with
    toPartialOrder := instPartialOrderOpenSubgroup }

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