image_setOf_minimal — Mathlib

English

If t ⊆ range f, the minimality of f x in t is equivalent to the minimality of x in t.

Русский

Если t ⊆ диапазон f, минимальность f x в t эквивалентна минимальности x в t.

LaTeX

$$$\\forall (ht : t \\subseteq \\operatorname{range} f),\\; \\operatorname{Minimal}(\\cdot \\in t) (f x) \\iff \\operatorname{Minimal}(\\cdot \\in t) x$$$

Lean4

theorem image_setOf_minimal (f : α ≃o β) (P : α → Prop) :
    f '' {x | Minimal P x} = {x | Minimal (fun x ↦ P (f.symm x)) x} :=
  by
  convert _root_.image_monotone_setOf_minimal (f := f) (by simp [f.le_iff_le])
  aesop

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