wellFoundedOn_image — Mathlib

English

The well-foundedness of the image f''s is equivalent to the well-foundedness of s under the transported relation r on f.

Русский

Хорошо основанность образа f'' s эквивалентна хорошо основанности множества s под переносимым отношением r на f.

LaTeX

$$(f'' s).WellFoundedOn r \\iff s.WellFoundedOn (r \\text{ on } f)$$

Lean4

@[simp]
theorem wellFoundedOn_image {s : Set β} : (f '' s).WellFoundedOn r ↔ s.WellFoundedOn (r on f) := by rw [image_eq_range];
  exact wellFoundedOn_range

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