mono — Mathlib

English

If t is WellFoundedOn r' and r ≤ r' and s ⊆ t, then s is WellFoundedOn r.

Русский

Если t хорошо основано относительно r', r≤r' и s ⊆ t, то s хорошо основано относительно r.

LaTeX

$$h : t.WellFoundedOn r' → le : r ≤ r' → hst : s ⊆ t → s.WellFoundedOn r$$

Lean4

protected theorem mono (h : t.WellFoundedOn r') (hle : r ≤ r') (hst : s ⊆ t) : s.WellFoundedOn r :=
  by
  rw [wellFoundedOn_iff] at *
  exact Subrelation.wf (fun xy => ⟨hle _ _ xy.1, hst xy.2.1, hst xy.2.2⟩) h

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