map_wcovBy — Mathlib

English

Let f be an order isomorphism. Then f(x) ⩿ f(y) holds exactly when x ⩿ y.

Русский

Пусть f — порядок-изоморфизм. Тогда f(x) покрывает f(y) тогда и только тогда, когда x покрывает y.

LaTeX

$$$$\forall {x,y}:\alpha,\ Iff(\mathrm{WCovBy}(f x,f y),\mathrm{WCovBy}(x,y)).$$$$

Lean4

theorem map_wcovBy {α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x y : α} : f x ⩿ f y ↔ x ⩿ y :=
  by
  use f.toOrderEmbedding.wcovBy_of_apply
  conv_lhs => rw [← f.symm_apply_apply x, ← f.symm_apply_apply y]
  exact f.symm.toOrderEmbedding.wcovBy_of_apply

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