exists — Mathlib

English

If for every x, Antitone (P x), then y ↦ ∃ x, P x y is antitone in y.

Русский

Если для каждого x предикат P x антимонотонен по y, то функция y ↦ ∃ x, P x y антимонотонна.

LaTeX

$$$\\\\forall y,z\\\\in \\\\alpha,\\\\ y \\\\le z \\\\Rightarrow (\\\\exists x, P x z) \\\\Rightarrow (\\\\exists x, P x y)$$$

Lean4

theorem «exists» {P : β → α → Prop} (hP : ∀ x, Antitone (P x)) : Antitone fun y => ∃ x, P x y := fun _ _ hy ⟨x, hx⟩ ↦
  ⟨x, hP x hy hx⟩

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