Theorem OrderEmbedding.wcovBy_of_apply

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 OrderEmbedding.wcovBy_of_apply View on Github →

2024-08-29 12:34

Mathlib/Order/Cover.lean

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

Added OrderEmbedding.wcovBy_of_apply View on Github →