instWellFoundedLT — Mathlib

English

If I is linearly ordered and WellFoundedLT[I], then WellFoundedLT(Products I).

Русский

Если I линейно упорядочено и имеет WellFoundedLT, тогда и у Products I имеется WellFoundedLT.

LaTeX

$$$$ \\text{WellFoundedLT}(\\mathrm{Products}\\, I). $$$$

Lean4

instance [WellFoundedLT I] : WellFoundedLT (Products I) :=
  by
  have : (· < · : Products I → _ → _) = (fun l m ↦ List.Lex (· < ·) l.val m.val) := by ext; exact lt_iff_lex_lt _ _
  rw [WellFoundedLT, this]
  dsimp [Products]
  rw [(by rfl : (· > · : I → _) = flip (· < ·))]
  infer_instance

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