Commit 2023-01-20 07:27 27b16657

View on Github →

feat: port Order.OmegaCompletePartialOrder (#1168)

depends on: #1397

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/CompleteLattice.lean

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Order/Hom/Order.lean

added theorem OrderHom.coe_inf

added theorem OrderHom.coe_sup

Created Mathlib/Order/OmegaCompletePartialOrder.lean

added theorem CompleteLattice.bot_continuous

added theorem CompleteLattice.inf_continuous'

added theorem CompleteLattice.inf_continuous

added theorem CompleteLattice.sup_continuous

added theorem CompleteLattice.supᵢ_continuous

added theorem CompleteLattice.supₛ_continuous'

added theorem CompleteLattice.supₛ_continuous

added theorem CompleteLattice.top_continuous

added theorem OmegaCompletePartialOrder.Chain.exists_of_mem_map

added def OmegaCompletePartialOrder.Chain.map

added theorem OmegaCompletePartialOrder.Chain.map_comp

added theorem OmegaCompletePartialOrder.Chain.map_id

added theorem OmegaCompletePartialOrder.Chain.map_le_map

added theorem OmegaCompletePartialOrder.Chain.mem_map

added theorem OmegaCompletePartialOrder.Chain.mem_map_iff

added def OmegaCompletePartialOrder.Chain.zip

added def OmegaCompletePartialOrder.Chain

added theorem OmegaCompletePartialOrder.Continuous'.to_bundled

added theorem OmegaCompletePartialOrder.Continuous'.to_monotone

added def OmegaCompletePartialOrder.Continuous'

added theorem OmegaCompletePartialOrder.Continuous.of_bundled'

added theorem OmegaCompletePartialOrder.Continuous.of_bundled

added def OmegaCompletePartialOrder.Continuous

added def OmegaCompletePartialOrder.ContinuousHom.Prod.apply

added def OmegaCompletePartialOrder.ContinuousHom.Simps.apply

added theorem OmegaCompletePartialOrder.ContinuousHom.apply_mono

added theorem OmegaCompletePartialOrder.ContinuousHom.bind_continuous'

added def OmegaCompletePartialOrder.ContinuousHom.comp

added theorem OmegaCompletePartialOrder.ContinuousHom.comp_assoc

added theorem OmegaCompletePartialOrder.ContinuousHom.comp_id

added theorem OmegaCompletePartialOrder.ContinuousHom.congr_arg

added theorem OmegaCompletePartialOrder.ContinuousHom.congr_fun

added def OmegaCompletePartialOrder.ContinuousHom.const

added theorem OmegaCompletePartialOrder.ContinuousHom.const_apply

added theorem OmegaCompletePartialOrder.ContinuousHom.continuous

added def OmegaCompletePartialOrder.ContinuousHom.flip

added theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge'

added theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge

added def OmegaCompletePartialOrder.ContinuousHom.id

added theorem OmegaCompletePartialOrder.ContinuousHom.id_comp

added theorem OmegaCompletePartialOrder.ContinuousHom.ite_continuous'

added theorem OmegaCompletePartialOrder.ContinuousHom.map_continuous'

added def OmegaCompletePartialOrder.ContinuousHom.ofFun

added def OmegaCompletePartialOrder.ContinuousHom.ofMono

added theorem OmegaCompletePartialOrder.ContinuousHom.ofMono_toFun

added theorem OmegaCompletePartialOrder.ContinuousHom.seq_continuous'

added def OmegaCompletePartialOrder.ContinuousHom.toMono

added theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_apply_ωSup

added theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_bind

added theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_def

added structure OmegaCompletePartialOrder.ContinuousHom

added theorem OmegaCompletePartialOrder.const_continuous'

added theorem OmegaCompletePartialOrder.continuous'_coe

added theorem OmegaCompletePartialOrder.continuous_comp

added theorem OmegaCompletePartialOrder.continuous_const

added theorem OmegaCompletePartialOrder.continuous_id

added theorem OmegaCompletePartialOrder.id_continuous'

added theorem OmegaCompletePartialOrder.le_ωSup_of_le

added def OmegaCompletePartialOrder.subtype

added theorem OmegaCompletePartialOrder.ωSup_le_iff

added theorem OmegaCompletePartialOrder.ωSup_le_ωSup_of_le

added theorem OmegaCompletePartialOrder.ωSup_total

added def OrderHom.bind

added theorem Part.eq_of_chain

added theorem Part.mem_chain_of_mem_ωSup

added theorem Part.mem_ωSup

added theorem Part.ωSup_eq_none

added theorem Part.ωSup_eq_some

added theorem Pi.OmegaCompletePartialOrder.flip₁_continuous'

added theorem Pi.OmegaCompletePartialOrder.flip₂_continuous'

added theorem Prod.ωSup_zip