mem_iSup — Mathlib

English

Membership in the supremum of a family of subsemigroups p i can be characterized by a universal property: m belongs to the supremum if and only if every common upper bound N contains m.

Русский

Членство в наибольшем элементе семейства подполугрупп p_i описывается через универсальное свойство: m ∈ ⨆ i, p_i iff для всякого общего верхнего Bound N верно m ∈ N.

LaTeX

$$$m \\in \\bigvee_{i} p_i \\;\\iff\\; \\forall N,\\ (\\forall i, p_i \\le N) \\rightarrow m \\in N$$$

Lean4

@[to_additive]
theorem mem_iSup {ι : Sort*} (p : ι → Subsemigroup M) {m : M} : (m ∈ ⨆ i, p i) ↔ ∀ N, (∀ i, p i ≤ N) → m ∈ N :=
  by
  rw [← closure_singleton_le_iff_mem, le_iSup_iff]
  simp only [closure_singleton_le_iff_mem]

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