Commit 2023-01-31 16:05 2769416a

View on Github →

chore(order/upper_lower): split file (#18330) This way we can port some topology.* files without wating for leanprover-community/mathlib4#1636 Also delete some lemmas that are true for any order_iso.

Estimated changes

Modified src/algebra/order/upper_lower.lean

Modified src/combinatorics/set_family/harris_kleitman.lean

Modified src/combinatorics/set_family/intersecting.lean

Modified src/combinatorics/young/young_diagram.lean

Modified src/order/countable_dense_linear_order.lean

Modified src/order/ideal.lean

Modified src/order/minimal.lean

Renamed src/order/upper_lower.lean to src/order/upper_lower/basic.lean

deleted def lower_set.Iic_Inf_hom

deleted theorem lower_set.Iic_Inf_hom_apply

modified theorem lower_set.Iic_inf

deleted def lower_set.Iic_inf_hom

deleted theorem lower_set.Iic_inf_hom_apply

deleted theorem lower_set.coe_Iic_Inf_hom

deleted theorem lower_set.coe_Iic_inf_hom

deleted def upper_set.Ici_Sup_hom

deleted theorem upper_set.Ici_Sup_hom_apply

modified theorem upper_set.Ici_sup

deleted def upper_set.Ici_sup_hom

deleted theorem upper_set.Ici_sup_hom_apply

Created src/order/upper_lower/hom.lean

added def lower_set.Iic_Inf_hom

added theorem lower_set.Iic_Inf_hom_apply

added def lower_set.Iic_inf_hom

added theorem lower_set.Iic_inf_hom_apply

added theorem lower_set.coe_Iic_Inf_hom

added theorem lower_set.coe_Iic_inf_hom

added def upper_set.Ici_Sup_hom

added theorem upper_set.Ici_Sup_hom_apply

added def upper_set.Ici_sup_hom

added theorem upper_set.Ici_sup_hom_apply

added theorem upper_set.coe_Ici_Sup_hom

added theorem upper_set.coe_Ici_sup_hom

Modified src/topology/order/lower_topology.lean

Modified src/topology/order/priestley.lean

Modified src/topology/sets/order.lean