Prove2Me

lean_workbook_plus_14910

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Given 0≤FX1(t)≤FX2(t)≤10 \leq F_{X_1}(t) \leq F_{X_2}(t) \leq 1 and 1≥1−FX1(t)≥1−FX2(t)≥01 \geq 1-F_{X_1}(t) \geq 1-F_{X_2}(t) \geq 0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14910 (F_X1 F_X2 : ℝ → ℝ) (t : ℝ) (h1 : 0 ≤ F_X1 t ∧ 0 ≤ F_X2 t) (h2 : F_X1 t ≤ F_X2 t) (h3 : 1 ≥ 1 - F_X1 t ∧ 1 ≥ 1 - F_X2 t) (h4 : 1 - F_X1 t ≥ 1 - F_X2 t) : 0 ≤ F_X1 t ∧ 0 ≤ F_X2 t ∧ F_X1 t ≤ F_X2 t ∧ 1 ≥ 1 - F_X1 t ∧ 1 ≥ 1 - F_X2 t ∧ 1 - F_X1 t ≥ 1 - F_X2 t   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph