cof_eq_lift — Mathlib

English

If f is a RelIso between relations r on α and s on β, then cof r and cof s are equal after lifting the cofariannce through the lift operation; i.e., lifts of cof r and cof s are equal.

Русский

Если f — изоморфизм отношений между α и β, сохраняющий структуру, то кофинальность сохраняется под лифтом: lift(cof r) = lift(cof s).

LaTeX

$$$\\operatorname{lift}(\\operatorname{cof} r) = \\operatorname{lift}(\\operatorname{cof} s)$$$

Lean4

theorem cof_eq_lift [IsRefl β s] (f : r ≃r s) : Cardinal.lift.{v} (Order.cof r) = Cardinal.lift.{u} (Order.cof s) :=
  have := f.toRelEmbedding.isRefl
  (f.cof_le_lift).antisymm (f.symm.cof_le_lift)

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