Theorems · Theorem · order theory

Set.WellFoundedOn.mapsTo

∀ {α : Type u_6} {β : Type u_7} {r : α → α → Prop} (f : β → α) {s : Set α} {t : Set β},
  Set.MapsTo f t s → s.WellFoundedOn r → t.WellFoundedOn (Function.onFun r f)

Defined in

Mathlib.Order.WellFoundedSet

Cited by

7 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms