index_strictAnti — Mathlib

English

If H < K, then K.index < H.index.

Русский

Если H строго меньше K, то их индексы удовлетворяют неравенству.

LaTeX

$$K.index < H.index$$

Lean4

@[to_additive (attr := gcongr)]
theorem index_strictAnti (h : H < K) [H.FiniteIndex] : K.index < H.index :=
  by
  have h0 : K.index ≠ 0 := (finiteIndex_of_le h.le).index_ne_zero
  apply lt_of_le_of_ne (index_antitone h.le)
  rw [← relIndex_mul_index h.le, Ne, eq_comm, mul_eq_right₀ h0, relIndex_eq_one]
  exact h.not_ge

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