subsingleton_iff_bot_or_pure — Mathlib

English

A filter is subsingleton iff it is equal to ⊥ or to pure a for some a.

Русский

Фильтр является подсинглетным тогда и только тогда, когда он равен ⊥ или равен чистому фильтру purity a для некоторого a.

LaTeX

$$$$ \forall {\alpha},\ (l.Subsingleton \iff l = \bot \lor \exists a, l = pure a) $$$$

Lean4

/-- A filter is a subsingleton iff it is equal to `⊥` or to `pure a` for some `a`. -/
theorem subsingleton_iff_bot_or_pure : l.Subsingleton ↔ l = ⊥ ∨ ∃ a, l = pure a :=
  by
  refine ⟨fun hl ↦ ?_, ?_⟩
  · exact (eq_or_neBot l).imp_right (@Subsingleton.exists_eq_pure _ _ · hl)
  · rintro (rfl | ⟨a, rfl⟩) <;> simp

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