Theorem OrderIso.map_covBy

Modification history

2025-11-08 03:04

Mathlib/Order/Cover.lean

chore(Order): deprecate `Codisjoint.ne_bot_of_ne_top'`, `OrderEmbedding.{w,}covBy_of_apply` and `OrderIso.map_{w,}covBy` (#28486)

Deleted OrderIso.map_covBy View on Github →

2024-08-29 12:34

Mathlib/Order/Cover.lean

feat(Order/*): `CovBy` and `OrderIso` (#16222) …

Added OrderIso.map_covBy View on Github →