inf_principal_eq_bot — Mathlib

English

For any f and s, the infimum f ⊓ 𝓟(s) equals ⊥ if and only if the complement s^c belongs to f.

Русский

Для любой пары f и s максимум: f ⊓ 𝓟(s) = ⊥ тогда и только тогда, когда комплемент s^c принадлежит f.

LaTeX

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

Lean4

theorem inf_principal_eq_bot {f : Filter α} {s : Set α} : f ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f :=
  by
  rw [← empty_mem_iff_bot, mem_inf_principal]
  simp only [mem_empty_iff_false, imp_false, compl_def]

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