exists — Mathlib

English

If for every x, Monotone (P x) then the map y ↦ ∃ x, P x y is monotone 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 y) \\\\Rightarrow (\\\\exists x, P x z)$$$

Lean4

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

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