instWellFoundedGTTrivial — Mathlib

English

For every a in a preorder, the relation WellFoundedGT (Estimator.trivial a) holds.

Русский

Для каждого элемента a в предрядке выполняется WellFoundedGT (Estimator.trivial a).

LaTeX

$$∀ a, WellFoundedGT (Estimator.trivial a)$$

Lean4

instance (a : α) : WellFoundedGT (Estimator.trivial a) :=
  let f : Estimator.trivial a ≃o Unit := RelIso.ofUniqueOfRefl _ _
  let f' : Estimator.trivial a ↪o Unit := f.toOrderEmbedding
  f'.wellFoundedGT

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