Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-18 05:39 58883e3e

View on Github →

feat(topology/ωCPO): define Scott topology in connection with ω-complete partial orders (#4037)

Estimated changes

Modified src/control/lawful_fix.lean

Modified src/order/basic.lean

added def as_linear_order

Modified src/order/bounded_lattice.lean

added theorem le_iff_imp

Modified src/order/complete_lattice.lean

added theorem Inf_le_Inf_of_forall_exists_le

added theorem Sup_le_Sup_of_forall_exists_le

Modified src/order/lattice.lean

added theorem inf_le_iff

added theorem le_sup_iff

Modified src/order/omega_complete_partial_order.lean

added theorem complete_lattice.Sup_continuous'

added theorem complete_lattice.Sup_continuous

added theorem complete_lattice.bot_continuous

added theorem complete_lattice.inf_continuous

added theorem complete_lattice.sup_continuous

added theorem complete_lattice.top_continuous

added theorem omega_complete_partial_order.continuous_hom.monotone

Modified src/order/preorder_hom.lean

added theorem preorder_hom.monotone

Modified src/tactic/monotonicity/basic.lean

Created src/topology/omega_complete_partial_order.lean

added def Scott.is_open

added theorem Scott.is_open_inter

added theorem Scott.is_open_sUnion

added theorem Scott.is_open_univ

added def Scott.is_ωSup

added def Scott

added theorem Scott_continuous_of_continuous

added theorem continuous_of_Scott_continuous

added theorem is_ωSup_ωSup

added def not_below

added theorem not_below_is_open