eventuallyLE

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#HasSubset.Subset.eventuallyLE

English

If s ⊆ t, then s ≤ᶠ[l] t for any filter l.

Русский

Если s ⊆ t, то s ≤ᶠ[l] t для любого фильтра l.

LaTeX

$$$$ s \\subseteq t \\Rightarrow s \\le^l t $$$$

Lean4

theorem eventuallyLE {α} {l : Filter α} {s t : Set α} (h : s ⊆ t) : s ≤ᶠ[l] t :=
  Filter.Eventually.of_forall h

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

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

Разделы

Аффилиация

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