inf_eq_bot_iff — Mathlib

English

For any two filters f and g on α, f ⊓ g = ⊥ if and only if there exist U ∈ f and V ∈ g with U ∩ V = ∅.

Русский

Для любых фильтров f,g на α выполняется: f ⊓ g = ⊥ тогда и только тогда, когда существуют U ∈ f и V ∈ g такие, что U ∩ V = ∅.

LaTeX

$$$f \sqcap g = \bot \iff \exists U \in f, \exists V \in g, U \cap V = \emptyset$$$

Lean4

theorem inf_eq_bot_iff {f g : Filter α} : f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅ := by
  simp only [← disjoint_iff, Filter.disjoint_iff, Set.disjoint_iff_inter_eq_empty]

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