mem_filter_iff — Mathlib

English

If l has a basis given by p and s, then t belongs to l iff there exists i with p(i) and s(i) ⊆ t.

Русский

Пусть у n есть базис p(i), s(i). Тогда t ∈ l тогда и только если существует i с p(i) и s(i) ⊆ t.

LaTeX

$$$t \in l \iff \exists i,\ p(i) \wedge s(i) \subseteq t$$$

Lean4

protected theorem mem_filter_iff (h : IsBasis p s) {U : Set α} : U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U := by
  simp only [IsBasis.filter, FilterBasis.mem_filter_iff, mem_filterBasis_iff, exists_exists_and_eq_and]

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