disjoint_pure_pure — Mathlib

English

Membership in a filter equals equality with infimum with principal of complement of the set.

Русский

Членство в фильтре эквивалентно равенству через инфимум с принципиальным фильтром по дополнению множества.

LaTeX

$$$s \\in f \\iff f \\inf \\mathcal{P}(s^c) = \\bot$$$

Lean4

@[simp]
theorem disjoint_pure_pure {x y : α} : Disjoint (pure x : Filter α) (pure y) ↔ x ≠ y := by
  simp only [← principal_singleton, disjoint_principal_principal, disjoint_singleton]

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