image_setOf_minimal — Mathlib

English

For an order-embedding f, the image of the set of x with Minimal(... in s) equals the set of x with Minimal(... in f'' s).

Русский

Для вложения порядка f образ множества x с Minimal(· ∈ s) равен множеству x с Minimal(· ∈ f'' s).

LaTeX

$$$\\forall f:\\, \\text{OrderEmbedding }\\alpha \\to \\beta,\\; f''\\{x \\mid \\operatorname{Minimal}(\\cdot \\in s) x\\} = \\{x \\mid \\operatorname{Minimal}(\\cdot \\in f'' s) x\\}$$$

Lean4

@[simp]
theorem image_setOf_minimal : f '' {x | Minimal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x} :=
  _root_.image_monotone_setOf_minimal (by simp [f.le_iff_le])

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