exists_ge_and_iff_exists — Mathlib

English

For any semilattice with sup, monotone P, the existence of an x with x0 ≤ x and P x is equivalent to the existence of some x with P x: (∃ x, x0 ≤ x ∧ P x) ⇔ ∃ x, P x.

Русский

Для полурешётки с объединением, монотонной функции P существование x с x0 ≤ x и P x эквивалентно существованию некоторого x с P x.

LaTeX

$$$\\exists x\\,(x_0 \\le x \\wedge P(x)) \\;\\iff\\; \\exists x\\, P(x)$$$

Lean4

theorem exists_ge_and_iff_exists {P : α → Prop} {x₀ : α} (hP : Monotone P) : (∃ x, x₀ ≤ x ∧ P x) ↔ ∃ x, P x :=
  ⟨fun h => h.imp fun _ h => h.2, fun ⟨x, hx⟩ => ⟨x ⊔ x₀, le_sup_right, hP le_sup_left hx⟩⟩

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