eventually_lift'_iff — Mathlib

English

If h is monotone, then the predicate p on β holds eventually in f.lift' h iff there exists t ∈ f with p holding for every y ∈ h t.

Русский

Если h монотонно, то свойство p(y) выполняется в f.lift' h по существованию t ∈ f такое, что для всех y ∈ h t выполняется p(y).

LaTeX

$$$ (hh : Monotone h) \\Rightarrow {p : \\beta \\to Prop} : (\\forall^\\infty y \\in (f.lift' h), p\,y) \\iff \\exists t \\in f, \\forall y \\in h t, p\,y $$$

Lean4

theorem eventually_lift'_iff (hh : Monotone h) {p : β → Prop} : (∀ᶠ y in f.lift' h, p y) ↔ ∃ t ∈ f, ∀ y ∈ h t, p y :=
  mem_lift'_sets hh

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