mono' — Mathlib

English

If r' a b → r a b whenever a,b ∈ s, then s.WellFoundedOn r → s.WellFoundedOn r'.

Русский

Если для всех a,b ∈ s верно, что r' a b → r a b, то из существующего WellFoundedOn r следует WellFoundedOn r' на s.

LaTeX

$$theorem mono' (h : ∀ (a) (_ : a ∈ s) (b) (_ : b ∈ s), r' a b → r a b) : s.WellFoundedOn r → s.WellFoundedOn r'$$

Lean4

theorem mono' (h : ∀ (a) (_ : a ∈ s) (b) (_ : b ∈ s), r' a b → r a b) : s.WellFoundedOn r → s.WellFoundedOn r' :=
  Subrelation.wf @fun a b => h _ a.2 _ b.2

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