raised_iff — Mathlib

English

Raised n m holds exactly when n ≤ m ≤ n+1.

Русский

Raised n m эквивалентно неравенствам n ≤ m ≤ n+1.

LaTeX

$$Raised(n,m) ↔ (n \le m ∧ m ≤ n + 1)$$

Lean4

theorem raised_iff {n m} : Raised n m ↔ n ≤ m ∧ m ≤ n + 1 :=
  by
  constructor
  · rintro (rfl | rfl)
    · exact ⟨le_rfl, Nat.le_succ _⟩
    · exact ⟨Nat.le_succ _, le_rfl⟩
  · rintro ⟨h₁, h₂⟩
    rcases eq_or_lt_of_le h₁ with (rfl | h₁)
    · exact Or.inl rfl
    · exact Or.inr (le_antisymm h₂ h₁)

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