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