Antisymmetry by linear arithmetic

2/4 ~10 minlean

Derive equality from two opposite inequalities over rationals.

4 lines · Lean 4

import Mathlib

example (x y : ℚ) (h₁ : x ≤ y) (h₂ : y ≤ x) : x = y := by
  sorry

Objectifs

Indices

Voir la solution

import Mathlib

example (x y : ℚ) (h₁ : x ≤ y) (h₂ : y ≤ x) : x = y := by
  linarith