eventually_pure

Mathlib.Order.Filter.Map

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

English

For any p, (∀ᶠ x in pure a, p x) ↔ p a.

Русский

Для любых p: (∀ᶠ x в чистом фильтре a, p x) эквивалентно p a.

LaTeX

$$∀ {a} {p}, (∀ᶠ x in pure a, p x) ↔ p a$$

Lean4

@[simp]
theorem eventually_pure {a : α} {p : α → Prop} : (∀ᶠ x in pure a, p x) ↔ p a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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