mem_iSup_iff — Mathlib

English

Let f_i be a family of lower sets of a, indexed by I. Then a belongs to the supremum of the family {f_i} if and only if there exists an index i with a ∈ f_i.

Русский

Пусть {f_i} — семейство нижних множеств α, индексируемое I. Тогда a ∈ ⨆_i f_i тогда и только тогда, когда существует индекс i such that a ∈ f_i.

LaTeX

$$$a \in \bigvee_{i} f(i) \iff \exists i, a \in f(i)$$$

Lean4

@[simp]
theorem mem_iSup_iff {f : ι → LowerSet α} : (a ∈ ⨆ i, f i) ↔ ∃ i, a ∈ f i :=
  by
  rw [← SetLike.mem_coe, coe_iSup]
  exact mem_iUnion

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