Def OrderIso.IciBot

Modification history

2026-03-21 16:01

Mathlib/Order/Interval/Set/OrderIso.lean

chore(Order/UpperLower/Principal): use `to_dual` (#36945) …

Deleted OrderIso.IciBot View on Github →

2024-04-14 10:41

Mathlib/Data/Set/Intervals/OrderIso.lean

chore: remove autoImplicit from more files (#11798) …

Modified OrderIso.IciBot View on Github →

2022-12-16 12:16

Mathlib/Data/Set/Intervals/OrderIso.lean

feat: port Data.Set.Intervals.OrderIso (#1067) …

Added OrderIso.IciBot View on Github →