degree_interpolate_lt — Mathlib

English

The degree of interpolate(s,v,r) is strictly less than card(s) in the preorder sense

Русский

Степень интерполяции строго меньше card(s) в смысле порядка

LaTeX

$$deg\bigl(\text{interpolate}(s,v,r)\bigr) < #s$$

Lean4

theorem degree_interpolate_lt (hvs : Set.InjOn v s) : (interpolate s v r).degree < #s :=
  by
  rw [Nat.cast_withBot]
  rcases eq_empty_or_nonempty s with (rfl | h)
  · rw [interpolate_empty, degree_zero, card_empty]
    exact WithBot.bot_lt_coe _
  · refine lt_of_le_of_lt (degree_interpolate_le _ hvs) ?_
    rw [Nat.cast_withBot, WithBot.coe_lt_coe]
    exact Nat.sub_lt (Nonempty.card_pos h) zero_lt_one

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