le_trans

Énoncé

∀ {a : ℝ} {b : ℝ} {c : ℝ} (h₁ : a ≤ b) (h₂ : b ≤ c), a ≤ c

Enchaîne deux inégalités larges. Démontré à partir de la transitivité stricte, pas admis.

Axiomes consommés

Cet énoncé dépend de 1 axiome, et d’aucun autre. La liste est relevée par le noyau lui-même (#print axioms), pas déclarée à la main.

• ax6_lt_trans

Vocabulaire admis : myLt, ℝ — les déclarations qui nomment ℝ et ses opérations, communes à toute la bibliothèque.

Code

/-- Transitivité de `≤`, démontrée à partir de la transitivité de `<` et de l'égalité.

`a ≤ b` est défini comme `a < b ∨ a = b`, d'où quatre cas. Trois donnent une inégalité stricte,
le dernier une égalité. -/
theorem le_trans {a b c : ℝ} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
  or_elim h₁
    (fun hab =>
      or_elim h₂
        (fun hbc => or_inl (ax6_lt_trans a b c hab hbc))
        (fun hbc => or_inl (eq_subst (motif := fun x => a < x) hbc hab)))
    (fun hab =>
      or_elim h₂
        (fun hbc => or_inl (eq_subst (motif := fun x => x < c) (eq_symm hab) hbc))
        (fun hbc => or_inr (eq_trans hab hbc)))