wellFoundedOn_range — Mathlib

English

The well-foundedness of the range of f is equivalent to the well-foundedness of the relation r on α transported along f.

Русский

Хорошо основанность образа функции f эквивалентна хорошо основанности отношения r на α, перенесённого по f.

LaTeX

$$(range f).WellFoundedOn r \\iff WellFounded (r \\text{ on } f)$$

Lean4

@[simp]
theorem wellFoundedOn_range : (range f).WellFoundedOn r ↔ WellFounded (r on f) :=
  by
  let f' : β → range f := fun c => ⟨f c, c, rfl⟩
  refine ⟨fun h => (InvImage.wf f' h).mono fun c c' => id, fun h => ⟨?_⟩⟩
  rintro ⟨_, c, rfl⟩
  refine Acc.of_downward_closed f' ?_ _ ?_
  · rintro _ ⟨_, c', rfl⟩ -
    exact ⟨c', rfl⟩
  · exact h.apply _

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