mem_iSup — Mathlib

English

For a family (p_i) of submonoids, m ∈ ⨆ i, p_i iff for every submonoid N, if p_i ≤ N for all i then m ∈ N.

Русский

Пусть (p_i) — семейство подмономов. Тогда m принадлежит верхней границе ⨆ i, p_i тогда и только тогда, когда для любого подмоном N, удовлетворяющего p_i ≤ N ∀i, имеем m ∈ N.

LaTeX

$$$m \\in \\bigsqcup_i p_i \\;\\;\\;\\; \\text{(используется iSup notation)} \\iff \\forall N,\\; (\\forall i, p_i \\le N) \\to m \\in N$$$

Lean4

@[to_additive]
theorem mem_iSup {ι : Sort*} (p : ι → Submonoid 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]

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