Subsingleton — Mathlib

English

A filter l on α is subsingleton exactly when there exists a subsingleton set s that belongs to l.

Русский

Фильтр l на α является подсинглетным тогда и только тогда, когда существует подсинглетное множество s, которое принадлежит l.

LaTeX

$$$l.Subsingleton \iff \exists s \in l, Set.Subsingleton s$$$

Lean4

/-- We say that a filter is a *subsingleton* if there exists a subsingleton set
that belongs to the filter. -/
protected def Subsingleton (l : Filter α) : Prop :=
  ∃ s ∈ l, Set.Subsingleton s

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