English
A minimal element in s corresponds to a minimal element in t under a structure-preserving isomorphism.
Русский
Минимальный элемент в s отображается в минимальный элемент в t через изоморфизм, сохраняющий порядок.
LaTeX
$$$\\forall f:\\, s \\cong_o t,\\; f.map_minimal_mem(x) \\Rightarrow \\text{Minimal}(\\cdot \\in t) (f x)$$$
Lean4
theorem map_minimal_mem (f : s ≃o t) (hx : Minimal (· ∈ s) x) : Minimal (· ∈ t) (f ⟨x, hx.prop⟩) := by
simpa only [show t = range (Subtype.val ∘ f) by simp, mem_univ, minimal_true_subtype, hx, true_imp_iff,
image_univ] using
OrderEmbedding.minimal_mem_image (f.toOrderEmbedding.trans (OrderEmbedding.subtype t)) (s := univ) (x :=
⟨x, hx.prop⟩)
