mem_iff — Mathlib

English

For IsBasis p s, a set U belongs to the filter iff there exists i with p(i) and s(i) ⊆ U.

Русский

Пусть дан IsBasis p s. Тогда U принадлежит фильтру, тогда существует i с p(i) и s(i) ⊆ U.

LaTeX

$$$U \in h.filter \iff \exists i,\ p(i) \wedge s(i) \subseteq U$$$

Lean4

/-- Definition of `HasBasis` unfolded with implicit set argument. -/
theorem mem_iff (hl : l.HasBasis p s) : t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t :=
  hl.mem_iff' t

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