clusterPt_sup — Mathlib

English

For filters F and G, ClusterPt x (F ⊔ G) holds if and only if ClusterPt x F or ClusterPt x G.

Русский

Для фильтров F и G: ClusterPt x (F ⊔ G) эквивалентно ClusterPt x F или ClusterPt x G.

LaTeX

$$$\operatorname{ClusterPt} x (F \uplus G) \iff \operatorname{ClusterPt} x F \lor \operatorname{ClusterPt} x G$$$

Lean4

theorem clusterPt_sup {F G : Filter X} : ClusterPt x (F ⊔ G) ↔ ClusterPt x F ∨ ClusterPt x G := by
  simp only [ClusterPt, inf_sup_left, sup_neBot]

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