lift'_closure_eq_bot — Mathlib

English

For any filter l, l.lift' closure = ⊥ iff l = ⊥.

Русский

Для любого фильтра l: l.lift' closure = ⊥ тогда и только тогда, когда l = ⊥.

LaTeX

$$$\\\\text{lift'}\\\\operatorname{closure} = \\\\bot \\\\iff \\\\ l = \\\\bot$$$

Lean4

@[simp]
theorem lift'_closure_eq_bot {l : Filter X} : l.lift' closure = ⊥ ↔ l = ⊥ :=
  ⟨fun h => bot_unique <| h ▸ l.le_lift'_closure, fun h =>
    h.symm ▸ by rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]⟩

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