disjoint_iff_left — Mathlib

English

Let l be a filter on α with a HasBasis p s. Then l and any other filter l′ are disjoint if and only if there exists an index i with p i such that the complement of s i belongs to l′.

Русский

Пусть l — фильтр на α с базисом HasBasis p s. Тогда l и любой другой фильтр l' несовместны тогда и только тогда, когда существует индекс i с p i, такое что комплемент множества s i принадлежит l'.

LaTeX

$$$ l \perp l' \iff \exists i,\ p(i) \land (s(i))^c \in l' $$$

Lean4

theorem disjoint_iff_left (h : l.HasBasis p s) : Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l' := by
  simp only [h.disjoint_iff l'.basis_sets, id, ← disjoint_principal_left,
    (hasBasis_principal _).disjoint_iff l'.basis_sets, true_and, Unique.exists_iff]

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