inf_principal_eq_bot_iff_comap — Mathlib

English

Let F be a filter on α and s a subset of α. Then F ⊓ 𝓟 s = ⊥ if and only if comap ((↑) : s → α) F = ⊥.

Русский

Пусть F — фильтр на α и s ⊆ α. Тогда F ⊓ 𝓟 s = ⊥ тогда и только тогда, когда comap ((↑) : s → α) F = ⊥.

LaTeX

$$$ F \inf 𝓟 s = \bot \iff \operatorname{comap} (\mathrm{Subtype.val}) F = \bot $$$

Lean4

theorem inf_principal_eq_bot_iff_comap {F : Filter α} {s : Set α} : F ⊓ 𝓟 s = ⊥ ↔ comap ((↑) : s → α) F = ⊥ := by
  rw [principal_eq_map_coe_top s, ← Filter.push_pull', inf_top_eq, map_eq_bot_iff]

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