minimal_mem_image_iff — Mathlib

English

For an OrderEmbedding f, the equivalence between minimal in s and minimal in image holds.

Русский

Для вложения порядка f существует эквивалентность между минимальным в s и минимальным в образе.

LaTeX

$$$\\forall (f:\\, \\alpha \\hookrightarrow\\beta),\\; (\\text{Minimal}(\\cdot \\in s) x) \\iff (\\text{Minimal}(\\cdot \\in f'' s) f(x))$$$

Lean4

theorem minimal_mem_image_iff (ha : a ∈ s) : Minimal (· ∈ f '' s) (f a) ↔ Minimal (· ∈ s) a :=
  _root_.minimal_mem_image_monotone_iff ha (by simp [f.le_iff_le])

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