eventually_cocardinal_ne

Mathlib.Order.Filter.Cocardinal

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

English

For any x, eventually a ≠ x.

Русский

Для каждого x почти всегда a не равно x.

LaTeX

$$eventually_cocardinal_ne (x) : ∀ᶠ a in cocardinal α hreg, a ≠ x$$

Lean4

theorem eventually_cocardinal_ne (x : α) : ∀ᶠ a in cocardinal α hreg, a ≠ x := by
  simpa [Set.finite_singleton x] using hreg.nat_lt 1

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

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

Разделы

Аффилиация

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