English
If f is an order-embedding and CovBy after applying f holds, then CovBy holds before applying f.
Русский
Если f — вложение порядка и CovBy после применения f выполняется, тогда CovBy до применения f также выполняется.
LaTeX
$$$ (f : \\alpha \\hookrightarrow o \\beta)\\, (h : CovBy (RelEmbedding.instFunLike.coe f a) (RelEmbedding.instFunLike.coe f b)) \\Rightarrow CovBy a b $$$
Lean4
theorem map_covBy {α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x y : α} : f x ⋖ f y ↔ x ⋖ y :=
by
use f.toOrderEmbedding.covBy_of_apply
conv_lhs => rw [← f.symm_apply_apply x, ← f.symm_apply_apply y]
exact f.symm.toOrderEmbedding.covBy_of_apply
