Mathlib Changelog
Changelog
About
Github
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