mapsTo — Mathlib

English

If f maps t into s and s is well-founded with respect to r, then t is well-founded with respect to the pullback relation r on f.

Русский

Если отображение f отправляет t в s и s хорошо основано относительно r, то t хорошо основано относительно отображаемого по f отношения r.

LaTeX

$$$\\text{MapsTo}(f, t, s) \\land t.WellFoundedOn(r \\text{ on } f) \\text{ follows from } s.WellFoundedOn(r)$$$

Lean4

theorem mapsTo {α β : Type*} {r : α → α → Prop} (f : β → α) {s : Set α} {t : Set β} (h : MapsTo f t s)
    (hw : s.WellFoundedOn r) : t.WellFoundedOn (r on f) := by exact InvImage.wf (fun x : t ↦ ⟨f x, h x.prop⟩) hw

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