clusterPt_iff_lift'_closure' — Mathlib

English

ClusterPt x F is equivalent to the nontrivial infimum of (F.lift' closure) and pure x.

Русский

ClusterPt x F эквивалентно не тривиальной конъюнкции (F.lift' closure) и pure x.

LaTeX

$$$ClusterPt\ x\ F \iff (F.lift' closure \cap Pure.x).NeBot$$$

Lean4

theorem clusterPt_iff_lift'_closure' {F : Filter X} : ClusterPt x F ↔ (F.lift' closure ⊓ pure x).NeBot :=
  by
  rw [clusterPt_iff_lift'_closure, inf_comm]
  constructor
  · intro h
    simp [h, pure_neBot]
  · intro h U hU
    simp_rw [← forall_mem_nonempty_iff_neBot, mem_inf_iff] at h
    simpa using h ({ x } ∩ U) ⟨{ x }, by simp, U, hU, rfl⟩

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