inter_consecutive — Mathlib

English

Ico n m ∩ Ico m l = ∅ for natural numbers n ≤ m ≤ l.

Русский

Ico n m ∩ Ico m l = ∅ при n ≤ m ≤ l.

LaTeX

$$$\forall (n,m,l):\, \operatorname{Ico}(n,m) \cap \operatorname{Ico}(m,l) = []$$$

Lean4

@[simp]
theorem inter_consecutive (n m l : ℕ) : Ico n m ∩ Ico m l = [] :=
  by
  apply eq_nil_iff_forall_not_mem.2
  intro a
  simp only [and_imp, not_and, not_lt, List.mem_inter_iff, List.Ico.mem]
  intro _ h₂ h₃
  exfalso
  exact not_lt_of_ge h₃ h₂

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