eventuallyConst_set — Mathlib

English

A set is eventually constant along a filter iff it is eventually always contained or eventually never contained.

Русский

Множество константно по фильтру тогда, когда оно либо почти всегда содержится, либо почти всегда не содержится.

LaTeX

$$$\\\\forall {l} {s : Set α},\\\\; EventuallyConst s l \\\\Leftrightarrow (\\\\forallᶠ x \\\\in l, x \\\\\\in s) \\\\lor (\\\\forallᶠ x \\\\in l, x \\\\\\notin s)$$$

Lean4

theorem eventuallyConst_set {s : Set α} : EventuallyConst s l ↔ (∀ᶠ x in l, x ∈ s) ∨ (∀ᶠ x in l, x ∉ s) :=
  eventuallyConst_pred

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