eventuallyConst_pred — Mathlib

English

With a HasBasis, EventuallyConst p l is equivalent to p holding eventually or not holding eventually.

Русский

С базисом HasBasis условие EventuallyConst p l эквивалентно тому, что p выполняется почти всюду или не выполняется почти всюду.

LaTeX

$$$\\\\forall {l} {p},\\\\; l.HasBasis p s \\\\Rightarrow \\\\text{EventuallyConst } p l \\\\Leftrightarrow (\\\\text{l.Eventually } p) \\\\lor (\\\\text{l.Eventually } (\\\\lnot p))$$$

Lean4

theorem eventuallyConst_pred {p : α → Prop} : EventuallyConst p l ↔ (∀ᶠ x in l, p x) ∨ (∀ᶠ x in l, ¬p x) := by
  simp [eventuallyConst_pred', or_comm, EventuallyEq]

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