apply_wcovBy_apply_iff — Mathlib

English

If the range of an order-embedding is OrdConnected, then lifting and lowering along f preserves the weak cover relation in both directions.

Русский

Если образ вложения порядка по функции f образует OrdConnected, то слабое покрытие сохраняется и обратно: f(a) ⩿ f(b) эквивалентно a ⩿ b.

LaTeX

$$$$\forall {\alpha \beta} [\text{Preorder }\alpha][\text{Preorder }\beta],\forall a,b:\alpha,\forall f:\alpha\hookrightarrow_{\mathrm{ord}}\beta,\ (\mathrm{range}(f)).\mathrm{OrdConnected} \Rightarrow (f(a)⩿f(b)\leftrightarrow a⩿b).$$$$

Lean4

theorem apply_wcovBy_apply_iff (f : α ↪o β) (h : (range f).OrdConnected) : f a ⩿ f b ↔ a ⩿ b :=
  ⟨fun h2 => h2.of_image f, fun hab => hab.image f h⟩

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