refl

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyLE.refl

English

For any l and any f, f is eventually less than or equal to itself along l.

Русский

Для любого фильтра l и любой функции f выполняется f ≤ᶠ[l] f.

LaTeX

$$λ l f, f ≤ᶠ[l] f$$

Lean4

@[refl]
theorem refl (l : Filter α) (f : α → β) : f ≤ᶠ[l] f :=
  EventuallyEq.rfl.le

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

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

Разделы

Аффилиация

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