mem_iSup — Mathlib

English

Let f be a function from an index set I to L, where L is a complete sublattice of Set X. An element x of X lies in the supremum over i of f(i) precisely when there exists some i with x ∈ f(i).

Русский

Пусть f: I → L задаёт семейство подмножеств L ⊆ P(X). Тогда элемент x∈X принадлежит сумме по индексу i дони f(i) тогда и только тогда, когда существует индекс i с x ∈ f(i).

LaTeX

$$$$ x \in \bigvee_{i\in I} f(i) \;\Leftrightarrow\; \exists i\in I,\ x \in f(i). $$$$

Lean4

@[simp]
theorem mem_iSup : x ∈ ⨆ i : I, f i ↔ ∃ i : I, x ∈ f i := by simp [← mem_subtype]

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