subsingleton_iff_exists_le_pure — Mathlib

English

In a nonempty α, l is subsingleton iff there exists a with l ≤ pure a.

Русский

В непустом α фильтр l является подсинглетным тогда и только тогда, когда существует a, для которого l ≤ pure a.

LaTeX

$$[Nonempty α] : l.Subsingleton \iff ∃ a, l ≤ pure a$$

Lean4

/-- In a nonempty type, a filter is a subsingleton iff
it is less than or equal to a pure filter. -/
theorem subsingleton_iff_exists_le_pure [Nonempty α] : l.Subsingleton ↔ ∃ a, l ≤ pure a :=
  by
  rcases eq_or_neBot l with rfl | hbot
  · simp
  · simp [subsingleton_iff_bot_or_pure, ← hbot.le_pure_iff, hbot.ne]

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