mem_of_eq_bot

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.mem_of_eq_bot

English

If f ⊓ 𝓟(s^c) = ⊥ then s ∈ f.

Русский

Если f ⊓ 𝓟(s^c) = ⊥, то s ∈ f.

LaTeX

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

Lean4

theorem mem_of_eq_bot {f : Filter α} {s : Set α} (h : f ⊓ 𝓟 sᶜ = ⊥) : s ∈ f := by
  rwa [inf_principal_eq_bot, compl_compl] at h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru