exists_eq_pure — Mathlib

English

If l is subsingleton and NeBot l, then there exists a such that l = pure a.

Русский

Если l — подсинглетный и l не⊥, то существует a, такой что l = pure a.

LaTeX

$$$[l.NeBot] (hl : l.Subsingleton) : \exists a, l = pure a$$$

Lean4

/-- A nontrivial subsingleton filter is equal to `pure a` for some `a`. -/
theorem exists_eq_pure [l.NeBot] (hl : l.Subsingleton) : ∃ a, l = pure a :=
  by
  rcases hl with ⟨s, hsl, hs⟩
  rcases exists_eq_singleton_iff_nonempty_subsingleton.2 ⟨nonempty_of_mem hsl, hs⟩ with ⟨a, rfl⟩
  refine ⟨a, (NeBot.le_pure_iff ‹_›).1 ?_⟩
  rwa [le_pure_iff]

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