eventually_one

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.eventually_one

English

For any predicate p on α, (∀ᶠ x in 1, p x) holds if and only if p(1) holds.

Русский

Для любого предиката p на α верно: p(x) выполняется постоянно в 1 тогда, когда p(1) верно.

LaTeX

$$$(\\forall \\!^\\!\\text{eventually } x \\in 1, p(x)) \\iff p(1)$$$

Lean4

@[to_additive (attr := simp)]
theorem eventually_one {p : α → Prop} : (∀ᶠ x in 1, p x) ↔ p 1 :=
  eventually_pure

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru