instSubNonemptyInterval — Mathlib

English

For appropriate α and NonemptyInterval elements s,t,a,b, subtraction is congruent with the underlying structure; in particular s.fst - t.snd ≤ s.snd - t.fst.

Русский

Для подходящих α и элементов s,t,a,b из NonemptyInterval вычитание согласуется с основной структурой; в частности выполняется неравенство s.fst - t.snd ≤ s.snd - t.fst.

LaTeX

$$$\forall s,t \in \mathrm{NonemptyInterval}(\alpha):\ (s.fst - t.snd) \le (s.snd - t.fst).$$$

Lean4

instance : Sub (NonemptyInterval α) :=
  ⟨fun s t => ⟨(s.fst - t.snd, s.snd - t.fst), tsub_le_tsub s.fst_le_snd t.fst_le_snd⟩⟩

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