clusterPt_iff_lift'_closure — Mathlib

English

ClusterPt x F is characterized by the relation pure x ≤ (F.lift' closure).

Русский

ClusterPt x F описывается как равенство чистого фильтра x и подъема closure фильтра F.

LaTeX

$$$\text{ClusterPt}(x,F) \iff \text{pure}(x) \le (F.lift' closure)$$$

Lean4

theorem clusterPt_iff_lift'_closure {F : Filter X} : ClusterPt x F ↔ pure x ≤ (F.lift' closure) := by
  simp_rw [clusterPt_iff_forall_mem_closure, (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id,
    singleton_subset_iff, true_and, exists_const]

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