Skip to content

Commit c727a02

Browse files
committed
split
1 parent eb59dc0 commit c727a02

6 files changed

Lines changed: 7 additions & 380 deletions

File tree

Mathlib.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5914,7 +5914,8 @@ public import Mathlib.Order.Cover
59145914
public import Mathlib.Order.Defs.LinearOrder
59155915
public import Mathlib.Order.Defs.PartialOrder
59165916
public import Mathlib.Order.Defs.Unbundled
5917-
public import Mathlib.Order.DirSupClosed
5917+
public import Mathlib.Order.DirSupClosed.Basic
5918+
public import Mathlib.Order.DirSupClosed.Finite
59185919
public import Mathlib.Order.Directed
59195920
public import Mathlib.Order.DirectedInverseSystem
59205921
public import Mathlib.Order.Disjoint

Mathlib/Order/DirSupClosed.lean

Lines changed: 0 additions & 376 deletions
This file was deleted.

Mathlib/Order/IsNormal.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Violeta Hernández Palacios
66
module
77

88
public import Mathlib.Dynamics.FixedPoints.Defs
9-
public import Mathlib.Order.DirSupClosed
9+
public import Mathlib.Order.DirSupClosed.Basic
1010
public import Mathlib.Order.SuccPred.CompleteLinearOrder
1111
public import Mathlib.Order.SuccPred.InitialSeg
1212

0 commit comments

Comments
 (0)