exists_le_and_iff_exists — Mathlib

English

If P is antitone on a semilattice with inf, then (∃ x, x ≤ x0 ∧ P x) ⇔ ∃ x, P x.

Русский

Если P антитонна на полурешётке с инф, то (∃ x, x ≤ x0 ∧ P x) эквивалентно ∃ x, P x.

LaTeX

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

Lean4

theorem exists_le_and_iff_exists {P : α → Prop} {x₀ : α} (hP : Antitone P) : (∃ x, x ≤ x₀ ∧ P x) ↔ ∃ x, P x :=
  exists_ge_and_iff_exists <| hP.dual_left

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