instIsTrichotomousSubtype — Mathlib

English

If r is well-founded on α, then the induced relation on the subtype p is well-founded.

Русский

Если r хорошо основано на α, то ограничение Subrel r p на подптипе p хорошо основано.

LaTeX

$$$ IsWellFounded(\\text{Subtype } p)\,(Subrel r p). $$$

Lean4

instance (r : α → α → Prop) [IsTrichotomous α r] (p : α → Prop) : IsTrichotomous _ (Subrel r p) :=
  ⟨fun x y => by rw [Subtype.eq_iff]; exact @IsTrichotomous.trichotomous α r _ x y⟩

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