mem_iInf — Mathlib

English

An element x lies in the infimum iInf of a family of subsemigroups iff it lies in every member of the family.

Русский

Элемент x лежит в iInf семейства подполугрупп тогда и только тогда, когда он лежит в каждой из них.

LaTeX

$$$x \\in iInf_{i} S(i) \\iff ∀ i, x \\in S(i)$$$

Lean4

@[to_additive]
theorem mem_iInf {ι : Sort*} {S : ι → Subsemigroup M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

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