not_disjoint — Mathlib

English

Let F be a nontrivial filter on a set α. If s and t belong to F, then s ∩ t ≠ ∅.

Русский

Пусть F — неботовый фильтр на α. Если s и t принадлежат F, то s ∩ t ≠ ∅.

LaTeX

$$$f \ne \bot \land s \in f \land t \in f \Rightarrow s \cap t \neq \emptyset$$$

Lean4

theorem not_disjoint (hf : f.NeBot) (hs : s ∈ f) (ht : t ∈ f) : ¬Disjoint s t := fun h =>
  not_disjoint_self_iff.2 hf <| Filter.disjoint_iff.2 ⟨s, hs, t, ht, h⟩

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