eventuallyLE_antisymm_iff — Mathlib

English

For PartialOrder β, l.EventuallyEq f g holds iff l.EventuallyLE f g and l.EventuallyLE g f hold.

Русский

Для частично упорядоченного β: f =ᶠ[l] g эквивалентно одновременным выполениям f ≤ᶠ[l] g и g ≤ᶠ[l] f.

LaTeX

$$$ f =ᶠ[l] g \\iff (f ≤ᶠ[l] g) ∧ (g ≤ᶠ[l] f) $$$

Lean4

theorem eventuallyLE_antisymm_iff [PartialOrder β] {l : Filter α} {f g : α → β} : f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f :=
  by simp only [EventuallyEq, EventuallyLE, le_antisymm_iff, eventually_and]

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