instInfSet — Mathlib

English

The infimum over a set S of subgroups is the intersection of those subgroups.

Русский

Наибольшая нижняя грань множества подгрупп равна пересечению всех этих подгрупп.

LaTeX

$$$\text{InfSet}(\text{Subgroup } G)$ with meet given by "intersection"$$

Lean4

@[to_additive]
instance : InfSet (Subgroup G) :=
  ⟨fun s =>
    { (⨅ S ∈ s, Subgroup.toSubmonoid S).copy (⋂ S ∈ s, ↑S) (by simp) with
      inv_mem' := fun {x} hx => Set.mem_biInter fun i h => i.inv_mem (by apply Set.mem_iInter₂.1 hx i h) }⟩

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