mem_iInf_iff — Mathlib

English

Let f_i be a family of lower sets of α. Then a belongs to the infimum of the family {f_i} if and only if a ∈ f_i for every i.

Русский

Пусть {f_i} — семейство нижних множеств α. Тогда a ∈ ⨅_i f_i тогда и только тогда, когда для каждого i имеет место a ∈ f_i.

LaTeX

$$$a \in \bigwedge_{i} f(i) \iff \forall i,\ a \in f(i)$$$

Lean4

@[simp]
theorem mem_iInf_iff {f : ι → LowerSet α} : (a ∈ ⨅ i, f i) ↔ ∀ i, a ∈ f i :=
  by
  rw [← SetLike.mem_coe, coe_iInf]
  exact mem_iInter

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