mem_iSup_iff — Mathlib

English

Let f_i be a family of upper sets f: ι → UpperSet α. An element a ∈ α belongs to the supremum ⨆ i, f i if and only if a ∈ f i for all i.

Русский

Пусть f_i задаёт семейство верхних множеств; тогда a принадлежит верхней границе ⨆ i f_i тогда и только тогда, когда для каждого i имеет место a ∈ f_i.

LaTeX

$$$ a \in \bigvee_{i} f_i \iff \forall i, a \in f_i $$$

Lean4

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

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