instUniqueOfSubsingleton

Mathlib.Algebra.Group.Subgroup.Lattice

URI: https://scilib.ai/kg/mathlib#Subgroup.instUniqueOfSubsingleton

English

For ι-indexed S i, x ∈ ⨅ i, S i iff ∀ i, x ∈ S i.

Русский

Для индексированного семейства подгрупп S i верно: x ∈ ⨅ i, S i тогда и только тогда, когда ∀ i, x ∈ S i.

LaTeX

$$$x \in \bigwedge_{i} S_i \iff \forall i, x \in S_i$$$

Lean4

@[to_additive]
instance [Subsingleton G] : Unique (Subgroup G) :=
  ⟨⟨⊥⟩, fun a => @Subsingleton.elim _ (subsingleton_iff.mpr ‹_›) a _⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru