inv_of_finiteDimensional — Mathlib

English

If r is finite dimensional, then r.inv is well-founded (there are no infinite descending chains in the inverse).

Русский

Если r конечнодименсионально, то r.inv есть хорошо основанное отношение (нет бесконечных нисходящих цепочек для обратной связи).

LaTeX

$$$$ r^{-1} \\text{ is well-founded } \\text{ whenever } r \\text{ is finite dimensional}. $$$$

Lean4

theorem inv_of_finiteDimensional [r.FiniteDimensional] : r.inv.IsWellFounded :=
  by
  rw [IsWellFounded, wellFounded_iff_isEmpty_descending_chain]
  refine ⟨fun ⟨f, hf⟩ ↦ ?_⟩
  let s := RelSeries.mk (r := r) ((RelSeries.longestOf r).length + 1) (f ·) (hf ·)
  exact (RelSeries.longestOf r).length.lt_succ_self.not_ge s.length_le_length_longestOf

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