apply_wcovBy_apply_iff — Mathlib

English

Let e be an order isomorphism between α and β. Then for all a,b, e(a) ⩿ e(b) if and only if a ⩿ b.

Русский

Пусть e — порядок-изоморфизм между α и β. Тогда для любых a,b выполняется: e(a) ⩿ e(b) тогда и только тогда, когда a ⩿ b.

LaTeX

$$$$\forall a,b:\alpha,\forall e:\mathsf{EquivLike}(E)\,\text{(order isomorphism)},\ e(a)⩿e(b)\iff a⩿b.$$$$

Lean4

@[simp]
theorem apply_wcovBy_apply_iff {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) : e a ⩿ e b ↔ a ⩿ b :=
  (ordConnected_range (e : α ≃o β)).apply_wcovBy_apply_iff ((e : α ≃o β) : α ↪o β)

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