eventuallyConst_set' — Mathlib

English

The eventual constancy of a set-valued function reduces to the set being almost surely either empty or universal.

Русский

Константность по множеству сводится к тому, что множество почти всюду либо пусто, либо равно всему пространству.

LaTeX

$$$\\\\forall {l} {s : Set α},\\\\; EventuallyConst s l \\\\Leftrightarrow (s =_l (\\\\emptyset)) \\\\lor (s =_l Un\\\\iv)$$$

Lean4

theorem eventuallyConst_set' {s : Set α} : EventuallyConst s l ↔ (s =ᶠ[l] (∅ : Set α)) ∨ s =ᶠ[l] univ :=
  eventuallyConst_pred'

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