disjoint_iff — Mathlib

English

Disjoint f g is equivalent to the existence of s ∈ f and t ∈ g with Disjoint s t.

Русский

Не пересекаются фильтры f и g тогда и только тогда, когда существуют s ∈ f, t ∈ g such that Disjoint s t.

LaTeX

$$Disjoint f g \iff ∃ s ∈ f, ∃ t ∈ g, Disjoint s t$$

Lean4

protected theorem disjoint_iff {f g : Filter α} : Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t := by
  simp only [disjoint_iff, ← empty_mem_iff_bot, mem_inf_iff, inf_eq_inter, bot_eq_empty, @eq_comm _ ∅]

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