ge_iff_eq'

Mathlib.Order.Filter.Basic

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

← MathLib Explorer

English

Let h: f ≤ᶠ[l] g. Then g ≤ᶠ[l] f iff g =ᶠ[l] f.

Русский

Пусть h: f ≤ᶠ[l] g. Тогда g ≤ᶠ[l] f эквивалентно g =ᶠ[l] f.

LaTeX

$$$ h : f ≤ᶠ[l] g \\Rightarrow (g ≤ᶠ[l] f) \\iff (g =ᶠ[l] f) $$$

Lean4

theorem ge_iff_eq' [PartialOrder β] {l : Filter α} {f g : α → β} (h : f ≤ᶠ[l] g) : g ≤ᶠ[l] f ↔ g =ᶠ[l] f :=
  ⟨fun h' => h'.antisymm h, EventuallyEq.le⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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