wcovBy_of_apply — Mathlib

English

If f is an order-embedding and f(x) ⩿ f(y), then x ⩿ y.

Русский

Если f — вложение порядка и f(x) покрывает f(y), то x покрывает y.

LaTeX

$$$$\forall f:\alpha\hookrightarrow_{\mathrm{ord}}\beta,\forall x,y:\alpha,\ f(x)⩿f(y)\Rightarrow x⩿y.$$$$

Lean4

theorem wcovBy_of_apply {α β : Type*} [Preorder α] [Preorder β] (f : α ↪o β) {x y : α} (h : f x ⩿ f y) : x ⩿ y :=
  by
  use f.le_iff_le.1 h.1
  intro a
  rw [← f.lt_iff_lt, ← f.lt_iff_lt]
  apply h.2

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