mid — Mathlib

English

Given i > j with i a prelimit, mid hi hj is an element strictly between j and i.

Русский

Пусть i > j и i является предлимитом, тогда mid hi hj лежит строго между j и i.

LaTeX

$$$middle$hi, hj$ \in \mathrm{Ioo}(j,i)$$$

Lean4

/-- Given `j < i` with `i` a prelimit, `IsSuccPrelimit.mid` picks an arbitrary element strictly
between `j` and `i`. -/
noncomputable def mid {i j : α} (hi : IsSuccPrelimit i) (hj : j < i) : Ioo j i :=
  Classical.indefiniteDescription _ ((not_covBy_iff hj).mp <| hi j)

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