OmegaCompletePartialOrder

📁 Source: Mathlib/Order/OmegaCompletePartialOrder.lean

Statistics

Metric	Count
Definitions instOmegaCompletePartialOrder, instFunLikeNat, instInhabited, instLE, instMembership, map, pair, zip, ContinuousHom, apply, apply, bind, comp, const, copy, flip, id, inst, instInhabited, map, ofFun, seq, toMono, toOrderHom, ωSup, omegaCompletePartialOrder, ωSup, iterateChain, instFunLikeContinuousHom, instPartialOrderContinuousHom, subtype, toPartialOrder, «term_→𝒄_», ωScottContinuous, ωSup, omegaCompletePartialOrder, ωSup, instOmegaCompletePartialOrder, ωSupImpl, instOmegaCompletePartialOrderForall	40
Theorems bot, iSup, inf, sSup, sup, top, directed, exists_of_mem_map, ext, ext_iff, instOrderHomClassNat, isChain_range, map_coe, map_comp, map_id, map_le_map, mem_map, mem_map_iff, pair_succ, pair_zero, pair_zip_pair, range_pair, zip_coe, apply_apply, apply_mono, bind_apply, coe_apply, coe_inj, coe_mk, coe_toOrderHom, comp_apply, comp_assoc, comp_id, congr_arg, congr_fun, const_apply, continuous, copy_apply, ext, ext_iff, flip_apply, forall_forall_merge, forall_forall_merge', id_apply, id_comp, map_apply, map_ωSup', monotone, ofFun_apply, seq_apply, toMono_coe, toOrderHom_eq_coe, ωScottContinuous, bind, map, seq, ωScottContinuous_apply, ωSup_apply, ωSup_apply_ωSup, ωSup_bind, ωSup_def, omegaCompletePartialOrder_ωSup_coe, ωSup_coe, ωSup_iterate_le_fixedPoint, ωSup_iterate_le_prefixedPoint, ωSup_iterate_mem_fixedPoint, instOrderHomClassContinuousHom, isLUB_range_ωSup, le_ωSup, le_ωSup_of_le, apply, apply₂, comp, const, fun_comp, fun_const, fun_id, id, isLUB, map_ωSup, map_ωSup_of_orderHom, monotone, monotone_map_ωSup, of_apply₂, of_map_ωSup_of_orderHom, of_monotone_map_ωSup, ωScottContinuous_iff_apply₂, ωScottContinuous_iff_map_ωSup_of_orderHom, ωScottContinuous_iff_monotone_map_ωSup, ωSup_eq_of_isLUB, ωSup_le, ωSup_le_iff, ωSup_le_ωSup_of_le, ωSup_total, eq_of_chain, mem_chain_of_mem_ωSup, mem_ωSup, ωSup_eq_none, ωSup_eq_some, prodMk, ωScottContinuous_fst, ωScottContinuous_snd, ωSupImpl_fst, ωSupImpl_snd, ωSup_fst, ωSup_snd, ωSup_zip, ωScottContinuous	108
Total	148

CompleteLattice

Definitions

Name	Category	Theorems
instOmegaCompletePartialOrder 📖	CompOp	604 math math: IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, Dynamics.netEntropyEntourage_monotone, Dynamics.netMaxcard_monotone_subset, Set.ncard_mono, Matroid.exists_isBasis_disjoint_isBasis_of_subset, NonUnitalAlgebra.gc, Metric.disjoint_ball_infDist, convexIndependent_set_iff_inter_convexHull_subset, essSup_le_of_ae_le, Dynamics.coverEntropyInfEntourage_antitone, OrdinalApprox.lfpApprox_mono_mid, IsLinearMap.image_convexHull, LocalizedModule.subsingleton_iff_disjoint, FirstOrder.Language.Substructure.closure_eq_of_isRelational, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, convexHull_insert, subset_closedConvexHull, Geometry.SimplicialComplex.vertex_mem_convexHull_iff, SimpleGraph.isBipartiteWith_neighborSet_disjoint, closedConvexHull_min, lowerSemicontinuousOn_biSup, rank_le_card_isVisible, PrimeSpectrum.localization_specComap_range, convexHull_multiset_sum, Geometry.SimplicialComplex.convexHull_subset_space, Set.Finite.ecard_strictMonoOn, BoxIntegral.Box.disjoint_splitCenterBox, Matroid.isBase_compl_iff_maximal_disjoint_isBase, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, Geometry.SimplicialComplex.mem_space_iff, lowerSemicontinuousWithinAt_iSup, AlgebraicGeometry.HasAffineProperty.affineAnd_le_affineAnd, MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAt, OrderHom.le_map_sup_fixedPoints, upperSemicontinuousAt_biInf, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, Matroid.disjointSum_comm, OrdinalApprox.gfp_mem_range_gfpApprox, Disjoint.exists_cthickenings, Convex.convex_remove_iff_notMem_convexHull_remove, ProjectiveSpectrum.gc_homogeneousIdeal, Matroid.eRk_mono, convexHull_eq_iInter, FirstOrder.Language.Substructure.fg_closure_singleton, MeasureTheory.pairwise_disjoint_fundamentalInterior, MeasureTheory.monotone_spanningSets, LinearMap.polar_antitone, HasCardinalLT.Set.functor_obj, PrimeSpectrum.gc, OrdinalApprox.gfpApprox_ord_mem_fixedPoint, Complex.convexHull_reProdIm, IsVisible.mem_convexHull_isVisible, MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le, LowerSemicontinuousOn.le_liminf, Matroid.IsBasis.contract_dep_iff, OrderHom.lfp_induction, OrderHom.lfp_le_gfp, AddAction.orbit.pairwiseDisjoint, Topology.RelCWComplex.pairwiseDisjoint', convexJoin_segments, Matroid.contract_isCocircuit_iff, FirstOrder.Language.Substructure.small_closure, Topology.RelCWComplex.disjoint_openCell_of_ne, FirstOrder.Language.Substructure.cg_def, Cardinal.mk_monotone, AddAction.IsBlock.disjoint_vadd_left, OrderIso.essSup_apply, OrderedFinpartition.disjoint, OrderHom.map_lfp, exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, exists_dist_slope_lt_pairwiseDisjoint_hasSum, LinearEquiv.dilatransvections_pow_mono, FirstOrder.Language.Substructure.mem_closure, Besicovitch.exist_disjoint_covering_families, IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal, MeasureTheory.exists_null_pairwise_disjoint_diff, convexHull_union_neg_eq_absConvexHull, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', Localization.localRingHom_injective_of_primesOver_eq_singleton, interior_convexHull_nonempty_iff_affineSpan_eq_top, OrderHom.gfp_const_inf_le, Matroid.IsBasis.contract_indep_iff, mem_absConvexHull_iff, Perfect.small_diam_splitting, mem_convexHull_pi, Geometry.SimplicialComplex.convexHull_inter_convexHull, HasCardinalLT.Set.cocone_pt, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, AffineBasis.convexHull_eq_nonneg_coord, FirstOrder.Language.Substructure.fg_closure, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', segment_subset_convexHull, convexHull_toCone_eq_sInf, lowerSemicontinuousOn_iSup, lowerSemicontinuous_iff_le_liminf, OrderHom.nextFixed_le, MulAction.IsBlock.disjoint_smul_of_ne, OrdinalApprox.le_gfpApprox_of_mem_fixedPoints, Balanced.convexHull, upperSemicontinuous_biInf, subset_absConvexHull, Matroid.IsMinor.exists_eq_contract_delete_disjoint, balancedHull_subset_convexHull_union_neg, Matroid.delete_eq_self_iff, CategoryTheory.IsGrothendieckAbelian.isomorphisms_le_pushouts_generatingMonomorphisms, Convex.convexHull_union, closedConvexHull_eq_closure_convexHull, Finset.mem_convexHull', subset_convexHull, Dynamics.coverEntropy_monotone, MulAction.isBlock_iff_smul_eq_or_disjoint, Convex.convexHull_subset_iff, AffineBasis.interior_convexHull, Matroid.contract_eq_self_iff, AlgebraicIndependent.adjoin_iff_disjoint, OrdinalApprox.gfpApprox_le, MeasureTheory.SignedMeasure.exists_isCompl_positive_negative, Geometry.SimplicialComplex.inter_subset_convexHull, convexJoin_segment_singleton, Matroid.isClosed_iff_isFlat, convexJoin_singleton_segment, convexHull_diam, Matroid.Coindep.delete_spanning_iff, subset_closedAbsConvexHull, Dynamics.netEntropyEntourage_antitone, Fin.Embedding.exists_embedding_disjoint_range_of_add_le_Nat_card, Finset.centerMass_id_mem_convexHull, OrderHom.gfp_le_map, Set.Finite.isCompact_convexHull, Finset.centerMass_id_mem_convexHull_of_nonpos, OrderHom.le_prevFixed, convexHull_add, Set.ecard_strictMono, affineSpan_convexHull, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, Cardinal.mk_strictMonoOn, MeasureTheory.disjoint_addFundamentalInterior_addFundamentalFrontier, Besicovitch.TauPackage.monotone_iUnionUpTo, MeasureTheory.hittingBtwn_apply_anti, CategoryTheory.MorphismProperty.le_ind, Set.encard_strictMono, Subgroup.leftCoset_cover_filter_FiniteIndex_aux, convexHull_basis_eq_stdSimplex, Ideal.disjoint_powers_iff_notMem, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms, Matroid.Indep.contract_dep_iff, Convex.radon_partition, LowerSemicontinuousWithinAt.le_liminf, IsOpen.exists_iUnion_isClosed, Matroid.cRk_mono, ConvexOn.bddAbove_convexHull, FirstOrder.Language.Substructure.fg_def, Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq, AddAction.IsBlock.disjoint_vadd_vadd_set, Matroid.closure_eq_subtypeClosure, Ideal.exists_le_prime_disjoint, Ideal.disjoint_map_primeCompl_iff_comap_le, upperSemicontinuousOn_iInf, AddAction.IsBlock.vadd_eq_vadd_or_disjoint, ConvexIndependent.mem_convexHull_iff, LowerSemicontinuousAt.le_liminf, not_disjoint_segment_convexHull_triple, convexHull_vadd, Matroid.closure_mono, FirstOrder.Language.Substructure.lift_card_closure_le_card_term, Disjoint.exists_open_convexes, OrdinalApprox.gfpApprox_add_one, AlgebraicGeometry.topologically_iso_le, exists_mem_interior_convexHull_affineBasis, Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes, essInf_antitone_measure, FirstOrder.Language.Substructure.mem_closure_iff_exists_term, Besicovitch.exist_finset_disjoint_balls_large_measure, closedAbsConvexHull_min, Caratheodory.mem_minCardFinsetOfMemConvexHull, totallyBounded_absConvexHull, Matroid.dual_indep_iff_exists', Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux, absConvexHull_nonempty, MeasureTheory.disjoint_fundamentalInterior_fundamentalFrontier, absConvexHull_empty, AddAction.IsBlock.pairwiseDisjoint_range_vadd, upperSemicontinuousWithinAt_iff_limsup_le, Set.Finite.card_strictMonoOn, absConvexHull_eq_self, UpperSemicontinuousWithinAt.limsup_le, OrderHom.isLeast_lfp, MulAction.orbit.eq_or_disjoint, Convex.mem_extremePoints_iff_mem_diff_convexHull_diff, CategoryTheory.SmallObject.succStruct_prop_le_propArrow, OrderHom.le_map_sSup_subset_fixedPoints, IsLocalization.isPrime_iff_isPrime_disjoint, SubMulAction.disjoint_val_image, PointedCone.dual_antitone, upperSemicontinuousOn_iff_limsup_le, Dynamics.coverMincard_antitone, NonUnitalStarAlgebra.gc, Dynamics.netMaxcard_antitone, AddAction.IsBlock.disjoint_vadd_set_vadd, mk_mem_convexHull_prod, AlgebraicGeometry.isCompl_range_inl_inr, Metric.disjoint_closedEBall_of_lt_infEDist, OrdinalApprox.lfpApprox_ord_eq_lfp, OrdinalApprox.lfpApprox_le_of_mem_fixedPoints, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, ProjectiveSpectrum.gc_set, OrderHom.gfp_le, convexHull_add_subset, ConvexCone.disjoint_hull_left_of_convex, EisensteinSeries.pairwise_disjoint_gammaSet, Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_card, closedConvexHull_closure_eq_closedConvexHull, MulAction.IsBlock.disjoint_smul_right, Polynomial.rootSet_derivative_subset_convexHull_rootSet, BoxIntegral.unitPartition.disjoint, AlgebraicGeometry.Scheme.mem_overGrothendieckTopology, closure_convexHull_extremePoints, MulAction.IsBlock.disjoint_smul_smul_set, Dynamics.coverEntropyEntourage_monotone, Set.Finite.isClosed_convexHull, NumberField.ComplexEmbedding.disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver, convexHull_empty, OrdinalApprox.lfpApprox_ord_mem_fixedPoint, absConvexHull_add_subset, Finset.centerMass_mem_convexHull, lowerSemicontinuous_iSup, convexHull_pair, preCantorSet_antitone, MeasureTheory.hittingBtwn_anti, OrdinalApprox.lfpApprox_monotone, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, Matroid.contract_spanning_iff, FirstOrder.Language.Substructure.mem_closed_of_isRelational, Topology.CWComplex.pairwiseDisjoint', Dynamics.coverEntropyInf_monotone, OrdinalApprox.gfpApprox_antitone, FirstOrder.Language.Substructure.fg_iff_exists_fin_generating_family, MulAction.IsBlock.disjoint_smul_set_smul, Matroid.closure_disjoint_of_disjoint_of_subset_coloops, convexJoin_subset_convexHull, Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull, convexHull_eq_empty, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, Vitali.exists_disjoint_subfamily_covering_enlargement_closedBall, MvPolynomial.supported_strictMono, AddAction.IsBlock.disjoint_vadd_right, convexHull_singleton, MeasureTheory.hittingAfter_apply_anti, OrderHom.lfp_lfp, UpperSemicontinuousOn.limsup_le, ωScottContinuous.iSup, upperSemicontinuous_iInf, OrdinalApprox.lfpApprox_add_one, convex_convexHull, OrderHom.le_lfp, convexHull_sum, OrdinalApprox.gfpApprox_ord_eq_gfp, FirstOrder.Language.Substructure.closure_insert, isBounded_convexHull, AddAction.isBlock_iff_vadd_eq_or_disjoint, Dynamics.netEntropyInfEntourage_monotone, Set.exists_union_disjoint_cardinal_eq_of_even, Finset.mem_convexHull, OrderHom.isFixedPt_lfp, essSup_mono_measure, convexHull_neg, convexIndependent_set_iff_notMem_convexHull_diff, OrderHom.gfp_gfp, LinearEquiv.transvections_pow_mono, convexHull_sphere_eq_closedBall, LowerSemicontinuous.le_liminf, LinearMap.polar_gc, Matroid.IsCircuit.disjoint_coloops, Subgroup.IsComplement.pairwiseDisjoint_smul, Convex.exists_subset_interior_convexHull_finset_of_isCompact, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, convexHull_mono, VitaliFamily.FineSubfamilyOn.covering_disjoint_subtype, convex_absConvexHull, OrderHom.nextFixed_le_iff, Cardinal.mk_strictMono, convexHullAddMonoidHom_apply, absConvexHull_mono, Finset.convexHull_eq, MulAction.IsBlock.smul_eq_smul_or_disjoint, ConvexCone.disjoint_coe, totallyBounded_convexHull, Set.Nonempty.absConvexHull, UpperSemicontinuousAt.limsup_le, AddAction.IsBlock.disjoint_vadd_of_ne, ωScottContinuous.sSup, Topology.RelCWComplex.disjoint_interior_base_closedCell, absConvex_convexClosedHull, upperSemicontinuousAt_iff_limsup_le, convexHull_eq_singleton, convexHull_eq_zero, OrderHom.map_le_lfp, Set.encard_mono, OrdinalApprox.lfpApprox_mono_left, SimpleGraph.IsBipartiteWith.disjoint, FirstOrder.Language.Substructure.closure_empty, isCompact_closedAbsConvexHull_of_totallyBounded, VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae, absConvexHull_subset_closedAbsConvexHull, Matroid.setOf_indep_eq, toWeakSpace_closedConvexHull_eq, convexHull_pi, FirstOrder.Language.monotone_distinctConstantsTheory, FirstOrder.Language.Substructure.iSup_eq_closure, disjoint_ball_closedBall_iff, Caratheodory.mem_convexHull_erase, Set.card_strictMono, upperSemicontinuous_iff_limsup_le, SimpleGraph.isBipartiteWith_neighborSet_disjoint', doublyStochastic_eq_convexHull_permMatrix, absConvexHull_eq_iInter, isSaddlePointOn_iff', VitaliFamily.covering, exists_open_convex_of_notMem, Finset.centroid_mem_convexHull, FirstOrder.Language.Substructure.closure_eq_of_le, AddAction.isBlock_iff_disjoint_vadd_of_ne, Vitali.exists_disjoint_subfamily_covering_enlargement, ωScottContinuous.sup, Matroid.coindep_contract_iff, AbsConvex.absConvexHull_subset_iff, AddSubgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq, Topology.RelCWComplex.disjointBase, MeasureTheory.hittingAfter_eq_sInf, MeasureTheory.Egorov.notConvergentSeq_antitone, OrderHom.map_gfp, Projectivization.Subspace.monotone_span, FirstOrder.Language.Substructure.subset_closure, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, FirstOrder.Language.Substructure.closure_iUnion, Metric.disjoint_closedBall_of_lt_infDist, absConvex_absConvexHull, Metric.frontier_thickening_disjoint, iSup₂_iInf₂_le_iInf₂_iSup₂, MulAction.isBlock_iff_smul_eq_smul_or_disjoint, AddAction.isBlock_iff_pairwiseDisjoint_range_vadd, ProjectiveSpectrum.gc_ideal, lowerSemicontinuousWithinAt_iff_le_liminf, Vitali.exists_disjoint_covering_ae, Matroid.Indep.eq_union_image_of_disjointSum, MulAction.IsBlock.disjoint_smul_left, Set.Infinite.exists_union_disjoint_cardinal_eq_of_infinite, LinearMap.image_convexHull, FirstOrder.Language.Substructure.closure_union, MulAction.isBlock_iff_disjoint_smul_of_ne, ContinuousMap.ideal_gc, ωScottContinuous.inf, Dynamics.coverEntropyEntourage_antitone, Besicovitch.exists_disjoint_closedBall_covering_ae, AddSubgroup.IsComplement.pairwiseDisjoint_vadd, PrimeSpectrum.gc_set, IsLocalization.orderIsoOfPrime_symm_apply_coe, StarAlgebra.gc, Matroid.dual_indep_iff_exists, convexHull_univ, convexHull_ediam, disjoint_closedBall_closedBall_iff, FirstOrder.Language.Structure.cg_iff, absConvexHull_min, lowerSemicontinuousAt_iff_le_liminf, AddAction.isBlock_iff_vadd_eq_vadd_or_disjoint, OrderIso.essInf_apply, OrdinalApprox.gfpApprox_mono_mid, HasCardinalLT.Set.cocone_ι_app, IsLocalization.disjoint_comap_iff, AffineIndependent.convexHull_inter', Polynomial.ringKrullDim_le, OrderHom.le_nextFixed, AddAction.orbit.eq_or_disjoint, convexHull_zero, OrderHom.le_prevFixed_iff, Matroid.IsBase.eq_union_image_of_disjointSum, convexHull_eq_union_convexHull_finite_subsets, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, Set.ncard_union_eq_iff, OrderHom.isGreatest_gfp_le, Topology.IsScott.ωScottContinuous_iff_continuous, Matroid.delete_dep_iff, MeasureTheory.exists_subordinate_pairwise_disjoint, zero_mem_absConvexHull, essInf_mono_ae, Matroid.contract_spanning_iff', Set.exists_union_disjoint_cardinal_eq_iff, HasCardinalLT.Set.functor_map_coe, affineCombination_mem_convexHull, upperSemicontinuousOn_biInf, Matroid.Indep.contract_indep_iff, mem_convexHull_iff_exists_fintype, Metric.frontier_cthickening_disjoint, MulAction.orbit.pairwiseDisjoint, absConvexHull_univ, MeasureTheory.hittingBtwn_eq_sInf, Topology.RelCWComplex.disjoint_skeleton_openCell, convexHull_toCone_isLeast, posTangentConeAt_mono, MeasureTheory.AEDisjoint.exists_disjoint_diff, MeasurableSpace.generateMeasurableRec_mono, disjoint_ball_ball_iff, extremePoints_convexHull_subset, MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection, Topology.RelCWComplex.disjointBase', OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq, Geometry.SimplicialComplex.face_subset_face_iff, OrdinalApprox.gfpApprox_mono_left, Convex.convexHull_eq, convexHull_convexHull_union_right, Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one, IsClosed.convexHull_subset_affineSpan_isVisible, upperSemicontinuousWithinAt_biInf, ConvexOn.le_sup_of_mem_convexHull, PiNat.disjoint_cylinder_of_longestPrefix_lt, OrderHom.prevFixed_le, HasCardinalLT.Set.instIsCardinalFiltered, SimpleGraph.disjoint_image_val_universalVerts, ConvexCone.disjoint_hull_right_of_convex, fixedPoints.lfp_eq_sSup_iterate, MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn, EMetric.disjoint_closedBall_of_lt_infEdist, FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize, Distribution.IsVanishingOn.disjoint_dsupport, AlgebraicGeometry.targetAffineLocally_affineAnd_le, Ideal.disjoint_primeCompl_of_liesOver, FirstOrder.Language.Substructure.closed, essSup_comp_le_essSup_map_measure, MulAction.IsBlock.pairwiseDisjoint_range_smul, MulAction.isBlock_iff_pairwiseDisjoint_range_smul, isSaddlePointOn_iff, absConvexHull_isClosed, DiffeologicalSpace.gc_generateFrom, Set.exists_union_disjoint_ncard_eq_of_even, convexHull_convexHull_union_left, convexHull_min, Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem, convexHull_isClosed, Matroid.delete_isBasis_iff, AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology, closedAbsConvexHull_eq_closure_absConvexHull, Matroid.isFlat_iff_isClosed, Matroid.closure_disjoint_coloops_of_disjoint_coloops, NumberField.InfinitePlace.disjoint_ramifiedPlacesOver_unramifiedPlacesOver, Matroid.IsCircuit.isCocircuit_disjoint_or_nontrivial_inter, PMF.toOuterMeasure_apply_eq_zero_iff, ConvexCone.gc_hull_coe, convexHull_prod, ωScottContinuous.top, FirstOrder.Language.Substructure.closure_withConstants_eq, AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, convexHull_eq_union, Topology.RelCWComplex.disjoint_skeletonLT_openCell, convexHull_eq, fixedPoints.gfp_eq_sInf_iterate, OrderHom.isGreatest_gfp, OrderHom.gfp_induction, convexHull_smul, ModelWithCorners.disjoint_interior_boundary, Set.Nonempty.convexHull, absConvexHull_eq_convexHull_balancedHull, FirstOrder.Language.Substructure.map_closure, Set.Finite.convexHull_eq_image, OrdinalApprox.lfp_mem_range_lfpApprox, AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom, OrderHom.map_sInf_subset_fixedPoints_le, mem_convexHull_of_exists_fintype, IsVisible.of_convexHull_of_pos, convexHull_rangle_single_eq_stdSimplex, FirstOrder.Language.Substructure.closure_le, AffineBasis.centroid_mem_interior_convexHull, AffineMap.image_convexHull, convexHull_union, convexHull_sub, FirstOrder.Language.Substructure.mem_closed_iff, SubAddAction.disjoint_val_image, lowerSemicontinuousAt_iSup, closure_subset_closedConvexHull, MeasureTheory.SimpleFunc.iSup_approx_apply, ConcaveOn.bddBelow_convexHull, Set.Countable.substructure_closure, MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd, FirstOrder.Language.Substructure.subset_closure_withConstants, convexHull_list_sum, essSup_mono_ae, Matroid.Indep.contract_isBase_iff, Set.Finite.ncard_strictMonoOn, AlgebraicGeometry.IsOpenImmersion.le_monomorphisms, IntermediateField.gc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.affineLocally_le, MulAction.IsBlock.smul_eq_or_disjoint, OrderHom.lfp_le, convexHull_nonempty_iff, disjoint_interior_extremePoints, RealRMK.range_cut_partition, Besicovitch.exists_disjoint_closedBall_covering_ae_aux, AffineIndependent.affineSpan_disjoint_of_disjoint, Ideal.exists_disjoint_powers_of_span_eq_top, Dynamics.netEntropyInfEntourage_antitone, MeasureTheory.pairwise_disjoint_addFundamentalInterior, upperSemicontinuousAt_iInf, Topology.RelCWComplex.pairwiseDisjoint, upperSemicontinuousWithinAt_iInf, Matroid.Coindep.delete_isBase_iff, closedAbsConvexHull_isClosed, HasCardinalLT.Set.instIsFilteredOfFactIsRegular, mem_convexHull_iff, Matroid.dualIndepMatroid_Indep, parallelepiped_eq_convexHull, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, lowerSemicontinuousWithinAt_biSup, OrdinalApprox.le_lfpApprox, PrimeSpectrum.localization_comap_range, IsLocalization.orderIsoOfPrime_apply_coe, ConvexOn.inf_le_of_mem_convexHull, lowerSemicontinuousAt_biSup, VitaliFamily.FineSubfamilyOn.covering_disjoint, absConvexHull_eq_empty, Matroid.IsBasis'.contract_dep_iff, Matroid.delete_indep_iff, FirstOrder.Language.Substructure.cg_iff_empty_or_exists_nat_generating_family, Disjoint.exists_thickenings, Matroid.Indep.disjoint_loops, AlgebraicGeometry.Scheme.propQCPrecoverage_monotone, MeasureTheory.hitting_eq_sInf, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, OrderHom.map_inf_fixedPoints_le, isClosed_closedAbsConvexHull, essSup_mono_measure', AffineIndependent.convexHull_inter, Urysohns.CU.disjoint_C_support_lim, convex_closedConvexHull, closure_subset_closedAbsConvexHull, IsLocalization.map_algebraMap_ne_top_iff_disjoint, AlgebraicGeometry.Scheme.codisjoint_zeroLocus, FirstOrder.Language.Hom.eqOn_closure, HasCardinalLT.Set.isFiltered_of_aleph0_le, Submodule.coe_scott_continuous, OrderHom.isFixedPt_gfp, Matroid.delete_isCircuit_iff, Set.Finite.convexHull_eq, OrderHom.isLeast_lfp_le, MeasureTheory.hittingAfter_anti, SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_notMem, Affine.Simplex.convexHull_eq_closedInterior, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, Set.ncard_strictMono, isClosed_closedConvexHull, OrderHom.map_lfp_comp, OrderHom.lfp_le_map, NumberField.InfinitePlace.disjoint_isReal_isComplex, Vitali.exists_disjoint_covering_ae', ωScottContinuous.bot, Set.Finite.encard_strictMonoOn, AddSubgroup.pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero, Matroid.IsBasis'.contract_indep_iff, lowerSemicontinuousOn_iff_le_liminf, OrderHom.lfp_le_fixed, Dynamics.coverEntropyInfEntourage_monotone, balanced_absConvexHull, convexHull_subset_affineSpan, convexHull_eq_self, disjoint_closedBall_ball_iff, OrderHom.le_gfp, IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal, balancedHull_convexHull_subseteq_absConvexHull, PiNat.exists_disjoint_cylinder, Algebra.gc, NumberField.mixedEmbedding.disjoint_negAt_plusPart, PMF.toMeasure_apply_eq_zero_iff, UpperSemicontinuous.limsup_le, convexHull_range_eq_exists_affineCombination, convexIndependent_iff_notMem_convexHull_diff, OrderHom.map_gfp_comp, Topology.RelCWComplex.disjoint_base_iUnion_openCell, AddAction.IsBlock.vadd_eq_or_disjoint, FirstOrder.Language.Substructure.lift_card_closure_le, FirstOrder.Language.Substructure.closure_eq, FirstOrder.Language.Substructure.mem_closure_iff_of_isRelational, FirstOrder.Language.Substructure.closure_mono, lowerSemicontinuous_biSup, FirstOrder.Language.Substructure.closure_univ, AlgebraicGeometry.sourceLocalClosure.le, FirstOrder.Language.Substructure.closure_image, AbsConvex.absConvexHull_eq, closedConvexHull_isClosed, Topology.RelCWComplex.disjoint_interior_base_iUnion_closedCell, le_essInf_of_ae_le, OrderHom.map_le_gfp, Matroid.setOf_dep_eq, closedAbsConvexHull_closure_eq_closedAbsConvexHull, AlgebraicGeometry.Spec.map_app, Complex.rectangle_eq_convexHull, FirstOrder.Language.Substructure.cg_closure_singleton, convexHull_subset_closedConvexHull, FirstOrder.Language.Structure.fg_iff, FirstOrder.Language.Substructure.cg_closure, Dynamics.coverMincard_monotone_subset, Finset.centerMass_mem_convexHull_of_nonpos

CompleteLattice.ωScottContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder Bot.bot Pi.instBotForall OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	sSup_empty sSup instIsEmptyFalse
iSup 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder iSup Pi.supSet CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup Monotone.iSup OmegaCompletePartialOrder.ωScottContinuous.monotone eq_of_forall_ge_iff iSup_apply OmegaCompletePartialOrder.ωScottContinuous.map_ωSup
inf 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder CompleteLinearOrder.toCompleteLattice	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder CompleteLinearOrder.toCompleteLattice Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice	—	OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup Monotone.inf OmegaCompletePartialOrder.ωScottContinuous.monotone eq_of_forall_ge_iff OmegaCompletePartialOrder.ωScottContinuous.map_ωSup le_trans OrderHom.mono le_max_left le_max_right
sSup 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder SupSet.sSup Pi.supSet CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	sSup_eq_iSup iSup
sup 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder Pi.instMaxForall_mathlib SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice	—	sSup_pair sSup
top 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder Top.top Pi.instTopForall OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup monotone_const eq_of_forall_ge_iff

OmegaCompletePartialOrder

Definitions

Name	Category	Theorems
ContinuousHom 📖	CompData	32 math math: ContinuousHom.const_apply, ContinuousHom.ωSup_apply, fixedPoints.ωSup_iterate_le_prefixedPoint, ContinuousHom.ωSup_apply_ωSup, instOrderHomClassContinuousHom, ContinuousHom.ωScottContinuous, ContinuousHom.apply_mono, ContinuousHom.bind_apply, ContinuousHom.seq_apply, ContinuousHom.ωScottContinuous_apply, ContinuousHom.copy_apply, ContinuousHom.coe_toOrderHom, ContinuousHom.coe_mk, ContinuousHom.forall_forall_merge, ContinuousHom.ofFun_apply, ContinuousHom.toOrderHom_eq_coe, ContinuousHom.id_apply, ContinuousHom.congr_fun, ContinuousHom.Prod.apply_apply, ContinuousHom.flip_apply, ContinuousHom.monotone, ContinuousHom.comp_apply, ContinuousHom.ext_iff, ContinuousHom.ωSup_def, ContinuousHom.congr_arg, ContinuousHom.forall_forall_merge', ContinuousHom.continuous, ContinuousHom.coe_apply, ContinuousHom.toMono_coe, fixedPoints.ωSup_iterate_le_fixedPoint, fixedPoints.ωSup_iterate_mem_fixedPoint, ContinuousHom.map_apply
instFunLikeContinuousHom 📖	CompOp	31 math math: ContinuousHom.const_apply, ContinuousHom.ωSup_apply, fixedPoints.ωSup_iterate_le_prefixedPoint, ContinuousHom.ωSup_apply_ωSup, instOrderHomClassContinuousHom, ContinuousHom.ωScottContinuous, ContinuousHom.apply_mono, ContinuousHom.bind_apply, ContinuousHom.seq_apply, ContinuousHom.ωScottContinuous_apply, ContinuousHom.copy_apply, ContinuousHom.coe_toOrderHom, ContinuousHom.coe_mk, ContinuousHom.forall_forall_merge, ContinuousHom.ofFun_apply, ContinuousHom.toOrderHom_eq_coe, ContinuousHom.id_apply, ContinuousHom.congr_fun, ContinuousHom.Prod.apply_apply, ContinuousHom.flip_apply, ContinuousHom.monotone, ContinuousHom.comp_apply, ContinuousHom.ext_iff, ContinuousHom.congr_arg, ContinuousHom.forall_forall_merge', ContinuousHom.continuous, ContinuousHom.coe_apply, ContinuousHom.toMono_coe, fixedPoints.ωSup_iterate_le_fixedPoint, fixedPoints.ωSup_iterate_mem_fixedPoint, ContinuousHom.map_apply
instPartialOrderContinuousHom 📖	CompOp	5 math math: ContinuousHom.ωSup_apply, ContinuousHom.ωSup_apply_ωSup, ContinuousHom.forall_forall_merge, ContinuousHom.forall_forall_merge', ContinuousHom.toMono_coe
subtype 📖	CompOp	—
toPartialOrder 📖	CompOp	641 math math: IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, Dynamics.netEntropyEntourage_monotone, Dynamics.netMaxcard_monotone_subset, Set.ncard_mono, Matroid.exists_isBasis_disjoint_isBasis_of_subset, NonUnitalAlgebra.gc, Metric.disjoint_ball_infDist, convexIndependent_set_iff_inter_convexHull_subset, essSup_le_of_ae_le, le_ωSup, Dynamics.coverEntropyInfEntourage_antitone, OrdinalApprox.lfpApprox_mono_mid, IsLinearMap.image_convexHull, LocalizedModule.subsingleton_iff_disjoint, FirstOrder.Language.Substructure.closure_eq_of_isRelational, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, convexHull_insert, subset_closedConvexHull, Geometry.SimplicialComplex.vertex_mem_convexHull_iff, SimpleGraph.isBipartiteWith_neighborSet_disjoint, closedConvexHull_min, lowerSemicontinuousOn_biSup, rank_le_card_isVisible, PrimeSpectrum.localization_specComap_range, convexHull_multiset_sum, Geometry.SimplicialComplex.convexHull_subset_space, Set.Finite.ecard_strictMonoOn, BoxIntegral.Box.disjoint_splitCenterBox, ContinuousHom.ωSup_apply, Matroid.isBase_compl_iff_maximal_disjoint_isBase, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, Geometry.SimplicialComplex.mem_space_iff, lowerSemicontinuousWithinAt_iSup, AlgebraicGeometry.HasAffineProperty.affineAnd_le_affineAnd, MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAt, ωSup_total, OrderHom.le_map_sup_fixedPoints, upperSemicontinuousAt_biInf, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, Matroid.disjointSum_comm, OrdinalApprox.gfp_mem_range_gfpApprox, Disjoint.exists_cthickenings, fixedPoints.ωSup_iterate_le_prefixedPoint, Convex.convex_remove_iff_notMem_convexHull_remove, ProjectiveSpectrum.gc_homogeneousIdeal, Matroid.eRk_mono, convexHull_eq_iInter, FirstOrder.Language.Substructure.fg_closure_singleton, MeasureTheory.pairwise_disjoint_fundamentalInterior, MeasureTheory.monotone_spanningSets, LinearMap.polar_antitone, HasCardinalLT.Set.functor_obj, PrimeSpectrum.gc, OrdinalApprox.gfpApprox_ord_mem_fixedPoint, Complex.convexHull_reProdIm, IsVisible.mem_convexHull_isVisible, MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le, LowerSemicontinuousOn.le_liminf, Matroid.IsBasis.contract_dep_iff, OrderHom.lfp_induction, OrderHom.lfp_le_gfp, AddAction.orbit.pairwiseDisjoint, Topology.RelCWComplex.pairwiseDisjoint', convexJoin_segments, Matroid.contract_isCocircuit_iff, FirstOrder.Language.Substructure.small_closure, Topology.RelCWComplex.disjoint_openCell_of_ne, ContinuousHom.ωSup_apply_ωSup, OrderHom.ωSup_coe, FirstOrder.Language.Substructure.cg_def, Cardinal.mk_monotone, AddAction.IsBlock.disjoint_vadd_left, OrderIso.essSup_apply, OrderedFinpartition.disjoint, OrderHom.map_lfp, exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, exists_dist_slope_lt_pairwiseDisjoint_hasSum, LinearEquiv.dilatransvections_pow_mono, FirstOrder.Language.Substructure.mem_closure, Besicovitch.exist_disjoint_covering_families, IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal, MeasureTheory.exists_null_pairwise_disjoint_diff, convexHull_union_neg_eq_absConvexHull, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', Localization.localRingHom_injective_of_primesOver_eq_singleton, interior_convexHull_nonempty_iff_affineSpan_eq_top, OrderHom.gfp_const_inf_le, Matroid.IsBasis.contract_indep_iff, mem_absConvexHull_iff, Perfect.small_diam_splitting, ωScottContinuous.map_ωSup_of_orderHom, mem_convexHull_pi, Geometry.SimplicialComplex.convexHull_inter_convexHull, HasCardinalLT.Set.cocone_pt, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, AffineBasis.convexHull_eq_nonneg_coord, FirstOrder.Language.Substructure.fg_closure, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', segment_subset_convexHull, convexHull_toCone_eq_sInf, lowerSemicontinuousOn_iSup, lowerSemicontinuous_iff_le_liminf, OrderHom.nextFixed_le, MulAction.IsBlock.disjoint_smul_of_ne, OrdinalApprox.le_gfpApprox_of_mem_fixedPoints, Balanced.convexHull, upperSemicontinuous_biInf, subset_absConvexHull, Matroid.IsMinor.exists_eq_contract_delete_disjoint, balancedHull_subset_convexHull_union_neg, Matroid.delete_eq_self_iff, CategoryTheory.IsGrothendieckAbelian.isomorphisms_le_pushouts_generatingMonomorphisms, Convex.convexHull_union, closedConvexHull_eq_closure_convexHull, Finset.mem_convexHull', subset_convexHull, Dynamics.coverEntropy_monotone, MulAction.isBlock_iff_smul_eq_or_disjoint, Convex.convexHull_subset_iff, AffineBasis.interior_convexHull, Matroid.contract_eq_self_iff, AlgebraicIndependent.adjoin_iff_disjoint, OrdinalApprox.gfpApprox_le, MeasureTheory.SignedMeasure.exists_isCompl_positive_negative, Geometry.SimplicialComplex.inter_subset_convexHull, convexJoin_segment_singleton, Matroid.isClosed_iff_isFlat, ωSup_le_iff, convexJoin_singleton_segment, convexHull_diam, Matroid.Coindep.delete_spanning_iff, Prod.ωSup_zip, subset_closedAbsConvexHull, Dynamics.netEntropyEntourage_antitone, Fin.Embedding.exists_embedding_disjoint_range_of_add_le_Nat_card, instOrderHomClassContinuousHom, Finset.centerMass_id_mem_convexHull, OrderHom.gfp_le_map, Set.Finite.isCompact_convexHull, Finset.centerMass_id_mem_convexHull_of_nonpos, OrderHom.le_prevFixed, convexHull_add, Set.ecard_strictMono, affineSpan_convexHull, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, Cardinal.mk_strictMonoOn, MeasureTheory.disjoint_addFundamentalInterior_addFundamentalFrontier, Besicovitch.TauPackage.monotone_iUnionUpTo, MeasureTheory.hittingBtwn_apply_anti, CategoryTheory.MorphismProperty.le_ind, Set.encard_strictMono, Subgroup.leftCoset_cover_filter_FiniteIndex_aux, convexHull_basis_eq_stdSimplex, Ideal.disjoint_powers_iff_notMem, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms, Matroid.Indep.contract_dep_iff, Convex.radon_partition, LowerSemicontinuousWithinAt.le_liminf, IsOpen.exists_iUnion_isClosed, Matroid.cRk_mono, ConvexOn.bddAbove_convexHull, FirstOrder.Language.Substructure.fg_def, Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq, ContinuousHom.apply_mono, AddAction.IsBlock.disjoint_vadd_vadd_set, Matroid.closure_eq_subtypeClosure, Ideal.exists_le_prime_disjoint, Ideal.disjoint_map_primeCompl_iff_comap_le, upperSemicontinuousOn_iInf, AddAction.IsBlock.vadd_eq_vadd_or_disjoint, ConvexIndependent.mem_convexHull_iff, LowerSemicontinuousAt.le_liminf, not_disjoint_segment_convexHull_triple, convexHull_vadd, Matroid.closure_mono, FirstOrder.Language.Substructure.lift_card_closure_le_card_term, Disjoint.exists_open_convexes, OrdinalApprox.gfpApprox_add_one, AlgebraicGeometry.topologically_iso_le, exists_mem_interior_convexHull_affineBasis, Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes, essInf_antitone_measure, FirstOrder.Language.Substructure.mem_closure_iff_exists_term, Besicovitch.exist_finset_disjoint_balls_large_measure, closedAbsConvexHull_min, Caratheodory.mem_minCardFinsetOfMemConvexHull, totallyBounded_absConvexHull, Matroid.dual_indep_iff_exists', Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux, absConvexHull_nonempty, MeasureTheory.disjoint_fundamentalInterior_fundamentalFrontier, absConvexHull_empty, AddAction.IsBlock.pairwiseDisjoint_range_vadd, upperSemicontinuousWithinAt_iff_limsup_le, Set.Finite.card_strictMonoOn, absConvexHull_eq_self, UpperSemicontinuousWithinAt.limsup_le, OrderHom.isLeast_lfp, MulAction.orbit.eq_or_disjoint, Convex.mem_extremePoints_iff_mem_diff_convexHull_diff, CategoryTheory.SmallObject.succStruct_prop_le_propArrow, OrderHom.le_map_sSup_subset_fixedPoints, IsLocalization.isPrime_iff_isPrime_disjoint, SubMulAction.disjoint_val_image, PointedCone.dual_antitone, upperSemicontinuousOn_iff_limsup_le, Dynamics.coverMincard_antitone, ωScottContinuous.map_ωSup, NonUnitalStarAlgebra.gc, Dynamics.netMaxcard_antitone, AddAction.IsBlock.disjoint_vadd_set_vadd, mk_mem_convexHull_prod, AlgebraicGeometry.isCompl_range_inl_inr, Metric.disjoint_closedEBall_of_lt_infEDist, OrdinalApprox.lfpApprox_ord_eq_lfp, OrdinalApprox.lfpApprox_le_of_mem_fixedPoints, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, ProjectiveSpectrum.gc_set, OrderHom.gfp_le, convexHull_add_subset, ConvexCone.disjoint_hull_left_of_convex, ωScottContinuous_iff_map_ωSup_of_orderHom, EisensteinSeries.pairwise_disjoint_gammaSet, Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_card, closedConvexHull_closure_eq_closedConvexHull, ContinuousHom.coe_toOrderHom, ContinuousHom.coe_mk, MulAction.IsBlock.disjoint_smul_right, Polynomial.rootSet_derivative_subset_convexHull_rootSet, BoxIntegral.unitPartition.disjoint, AlgebraicGeometry.Scheme.mem_overGrothendieckTopology, closure_convexHull_extremePoints, MulAction.IsBlock.disjoint_smul_smul_set, ContinuousHom.forall_forall_merge, Dynamics.coverEntropyEntourage_monotone, Set.Finite.isClosed_convexHull, NumberField.ComplexEmbedding.disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver, convexHull_empty, OrdinalApprox.lfpApprox_ord_mem_fixedPoint, absConvexHull_add_subset, Finset.centerMass_mem_convexHull, lowerSemicontinuous_iSup, convexHull_pair, preCantorSet_antitone, MeasureTheory.hittingBtwn_anti, OrdinalApprox.lfpApprox_monotone, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, Matroid.contract_spanning_iff, FirstOrder.Language.Substructure.mem_closed_of_isRelational, Topology.CWComplex.pairwiseDisjoint', Dynamics.coverEntropyInf_monotone, OrdinalApprox.gfpApprox_antitone, FirstOrder.Language.Substructure.fg_iff_exists_fin_generating_family, MulAction.IsBlock.disjoint_smul_set_smul, Matroid.closure_disjoint_of_disjoint_of_subset_coloops, convexJoin_subset_convexHull, Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull, convexHull_eq_empty, ωSup_le, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, Vitali.exists_disjoint_subfamily_covering_enlargement_closedBall, MvPolynomial.supported_strictMono, AddAction.IsBlock.disjoint_vadd_right, convexHull_singleton, ωScottContinuous_iff_monotone_map_ωSup, MeasureTheory.hittingAfter_apply_anti, Pi.ωScottContinuous_uncurry, OrderHom.lfp_lfp, UpperSemicontinuousOn.limsup_le, upperSemicontinuous_iInf, OrdinalApprox.lfpApprox_add_one, convex_convexHull, OrderHom.le_lfp, convexHull_sum, OrdinalApprox.gfpApprox_ord_eq_gfp, FirstOrder.Language.Substructure.closure_insert, isBounded_convexHull, AddAction.isBlock_iff_vadd_eq_or_disjoint, Dynamics.netEntropyInfEntourage_monotone, Set.exists_union_disjoint_cardinal_eq_of_even, Finset.mem_convexHull, OrderHom.isFixedPt_lfp, essSup_mono_measure, convexHull_neg, convexIndependent_set_iff_notMem_convexHull_diff, OrderHom.gfp_gfp, LinearEquiv.transvections_pow_mono, convexHull_sphere_eq_closedBall, LowerSemicontinuous.le_liminf, LinearMap.polar_gc, Matroid.IsCircuit.disjoint_coloops, Subgroup.IsComplement.pairwiseDisjoint_smul, Convex.exists_subset_interior_convexHull_finset_of_isCompact, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, convexHull_mono, VitaliFamily.FineSubfamilyOn.covering_disjoint_subtype, convex_absConvexHull, OrderHom.nextFixed_le_iff, Cardinal.mk_strictMono, convexHullAddMonoidHom_apply, absConvexHull_mono, Finset.convexHull_eq, MulAction.IsBlock.smul_eq_smul_or_disjoint, ConvexCone.disjoint_coe, totallyBounded_convexHull, Set.Nonempty.absConvexHull, UpperSemicontinuousAt.limsup_le, AddAction.IsBlock.disjoint_vadd_of_ne, Topology.RelCWComplex.disjoint_interior_base_closedCell, absConvex_convexClosedHull, upperSemicontinuousAt_iff_limsup_le, isωSup_ωSup, convexHull_eq_singleton, convexHull_eq_zero, OrderHom.map_le_lfp, Set.encard_mono, OrdinalApprox.lfpApprox_mono_left, SimpleGraph.IsBipartiteWith.disjoint, FirstOrder.Language.Substructure.closure_empty, isCompact_closedAbsConvexHull_of_totallyBounded, VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae, absConvexHull_subset_closedAbsConvexHull, ωScottContinuous.monotone_map_ωSup, Matroid.setOf_indep_eq, toWeakSpace_closedConvexHull_eq, convexHull_pi, FirstOrder.Language.monotone_distinctConstantsTheory, FirstOrder.Language.Substructure.iSup_eq_closure, disjoint_ball_closedBall_iff, ContinuousHom.toOrderHom_eq_coe, Caratheodory.mem_convexHull_erase, Set.card_strictMono, upperSemicontinuous_iff_limsup_le, SimpleGraph.isBipartiteWith_neighborSet_disjoint', doublyStochastic_eq_convexHull_permMatrix, absConvexHull_eq_iInter, isSaddlePointOn_iff', VitaliFamily.covering, exists_open_convex_of_notMem, Finset.centroid_mem_convexHull, FirstOrder.Language.Substructure.closure_eq_of_le, AddAction.isBlock_iff_disjoint_vadd_of_ne, Vitali.exists_disjoint_subfamily_covering_enlargement, Matroid.coindep_contract_iff, AbsConvex.absConvexHull_subset_iff, AddSubgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq, Topology.RelCWComplex.disjointBase, MeasureTheory.hittingAfter_eq_sInf, MeasureTheory.Egorov.notConvergentSeq_antitone, OrderHom.map_gfp, Projectivization.Subspace.monotone_span, FirstOrder.Language.Substructure.subset_closure, ωSup_le_ωSup_of_le, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, FirstOrder.Language.Substructure.closure_iUnion, Metric.disjoint_closedBall_of_lt_infDist, absConvex_absConvexHull, Metric.frontier_thickening_disjoint, iSup₂_iInf₂_le_iInf₂_iSup₂, MulAction.isBlock_iff_smul_eq_smul_or_disjoint, AddAction.isBlock_iff_pairwiseDisjoint_range_vadd, ProjectiveSpectrum.gc_ideal, lowerSemicontinuousWithinAt_iff_le_liminf, Vitali.exists_disjoint_covering_ae, Matroid.Indep.eq_union_image_of_disjointSum, MulAction.IsBlock.disjoint_smul_left, Set.Infinite.exists_union_disjoint_cardinal_eq_of_infinite, ωScottContinuous.isLUB, LinearMap.image_convexHull, FirstOrder.Language.Substructure.closure_union, MulAction.isBlock_iff_disjoint_smul_of_ne, ContinuousMap.ideal_gc, Dynamics.coverEntropyEntourage_antitone, Besicovitch.exists_disjoint_closedBall_covering_ae, AddSubgroup.IsComplement.pairwiseDisjoint_vadd, PrimeSpectrum.gc_set, IsLocalization.orderIsoOfPrime_symm_apply_coe, StarAlgebra.gc, Matroid.dual_indep_iff_exists, convexHull_univ, convexHull_ediam, disjoint_closedBall_closedBall_iff, FirstOrder.Language.Structure.cg_iff, absConvexHull_min, ContinuousHom.monotone, lowerSemicontinuousAt_iff_le_liminf, AddAction.isBlock_iff_vadd_eq_vadd_or_disjoint, OrderIso.essInf_apply, OrdinalApprox.gfpApprox_mono_mid, HasCardinalLT.Set.cocone_ι_app, IsLocalization.disjoint_comap_iff, AffineIndependent.convexHull_inter', Polynomial.ringKrullDim_le, OrderHom.le_nextFixed, AddAction.orbit.eq_or_disjoint, convexHull_zero, OrderHom.le_prevFixed_iff, Matroid.IsBase.eq_union_image_of_disjointSum, convexHull_eq_union_convexHull_finite_subsets, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, Set.ncard_union_eq_iff, ContinuousHom.ωSup_bind, OrderHom.isGreatest_gfp_le, ωScottContinuous.monotone, Matroid.delete_dep_iff, MeasureTheory.exists_subordinate_pairwise_disjoint, zero_mem_absConvexHull, essInf_mono_ae, Matroid.contract_spanning_iff', Set.exists_union_disjoint_cardinal_eq_iff, HasCardinalLT.Set.functor_map_coe, affineCombination_mem_convexHull, upperSemicontinuousOn_biInf, Matroid.Indep.contract_indep_iff, mem_convexHull_iff_exists_fintype, Metric.frontier_cthickening_disjoint, MulAction.orbit.pairwiseDisjoint, absConvexHull_univ, MeasureTheory.hittingBtwn_eq_sInf, Topology.RelCWComplex.disjoint_skeleton_openCell, convexHull_toCone_isLeast, posTangentConeAt_mono, MeasureTheory.AEDisjoint.exists_disjoint_diff, MeasurableSpace.generateMeasurableRec_mono, disjoint_ball_ball_iff, extremePoints_convexHull_subset, MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection, Topology.RelCWComplex.disjointBase', OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq, Geometry.SimplicialComplex.face_subset_face_iff, OrdinalApprox.gfpApprox_mono_left, Convex.convexHull_eq, convexHull_convexHull_union_right, Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one, IsClosed.convexHull_subset_affineSpan_isVisible, upperSemicontinuousWithinAt_biInf, ConvexOn.le_sup_of_mem_convexHull, PiNat.disjoint_cylinder_of_longestPrefix_lt, OrderHom.prevFixed_le, HasCardinalLT.Set.instIsCardinalFiltered, ωScottContinuous.of_map_ωSup_of_orderHom, SimpleGraph.disjoint_image_val_universalVerts, ConvexCone.disjoint_hull_right_of_convex, fixedPoints.lfp_eq_sSup_iterate, MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn, EMetric.disjoint_closedBall_of_lt_infEdist, FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize, Distribution.IsVanishingOn.disjoint_dsupport, AlgebraicGeometry.targetAffineLocally_affineAnd_le, Ideal.disjoint_primeCompl_of_liesOver, FirstOrder.Language.Substructure.closed, Prod.ωSup_snd, essSup_comp_le_essSup_map_measure, MulAction.IsBlock.pairwiseDisjoint_range_smul, MulAction.isBlock_iff_pairwiseDisjoint_range_smul, isSaddlePointOn_iff, absConvexHull_isClosed, DiffeologicalSpace.gc_generateFrom, Set.exists_union_disjoint_ncard_eq_of_even, convexHull_convexHull_union_left, convexHull_min, Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem, convexHull_isClosed, Matroid.delete_isBasis_iff, AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology, ContinuousHom.forall_forall_merge', closedAbsConvexHull_eq_closure_absConvexHull, Prod.ωSupImpl_fst, Matroid.isFlat_iff_isClosed, Matroid.closure_disjoint_coloops_of_disjoint_coloops, NumberField.InfinitePlace.disjoint_ramifiedPlacesOver_unramifiedPlacesOver, Matroid.IsCircuit.isCocircuit_disjoint_or_nontrivial_inter, PMF.toOuterMeasure_apply_eq_zero_iff, ConvexCone.gc_hull_coe, convexHull_prod, ContinuousHom.continuous, FirstOrder.Language.Substructure.closure_withConstants_eq, AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, convexHull_eq_union, Topology.RelCWComplex.disjoint_skeletonLT_openCell, convexHull_eq, fixedPoints.gfp_eq_sInf_iterate, OrderHom.isGreatest_gfp, OrderHom.gfp_induction, convexHull_smul, ModelWithCorners.disjoint_interior_boundary, Set.Nonempty.convexHull, absConvexHull_eq_convexHull_balancedHull, FirstOrder.Language.Substructure.map_closure, Pi.ωScottContinuous_curry, Set.Finite.convexHull_eq_image, ContinuousHom.coe_apply, OrdinalApprox.lfp_mem_range_lfpApprox, AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom, OrderHom.map_sInf_subset_fixedPoints_le, mem_convexHull_of_exists_fintype, IsVisible.of_convexHull_of_pos, ContinuousHom.toMono_coe, convexHull_rangle_single_eq_stdSimplex, FirstOrder.Language.Substructure.closure_le, AffineBasis.centroid_mem_interior_convexHull, AffineMap.image_convexHull, convexHull_union, convexHull_sub, FirstOrder.Language.Substructure.mem_closed_iff, SubAddAction.disjoint_val_image, Pi.uncurry_curry_ωScottContinuous, lowerSemicontinuousAt_iSup, closure_subset_closedConvexHull, MeasureTheory.SimpleFunc.iSup_approx_apply, ConcaveOn.bddBelow_convexHull, Set.Countable.substructure_closure, MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd, FirstOrder.Language.Substructure.subset_closure_withConstants, convexHull_list_sum, essSup_mono_ae, Matroid.Indep.contract_isBase_iff, Set.Finite.ncard_strictMonoOn, AlgebraicGeometry.IsOpenImmersion.le_monomorphisms, IntermediateField.gc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.affineLocally_le, MulAction.IsBlock.smul_eq_or_disjoint, OrderHom.lfp_le, convexHull_nonempty_iff, Prod.ωSup_fst, disjoint_interior_extremePoints, RealRMK.range_cut_partition, Besicovitch.exists_disjoint_closedBall_covering_ae_aux, AffineIndependent.affineSpan_disjoint_of_disjoint, Ideal.exists_disjoint_powers_of_span_eq_top, Dynamics.netEntropyInfEntourage_antitone, MeasureTheory.pairwise_disjoint_addFundamentalInterior, upperSemicontinuousAt_iInf, Topology.RelCWComplex.pairwiseDisjoint, upperSemicontinuousWithinAt_iInf, Matroid.Coindep.delete_isBase_iff, closedAbsConvexHull_isClosed, HasCardinalLT.Set.instIsFilteredOfFactIsRegular, mem_convexHull_iff, Matroid.dualIndepMatroid_Indep, parallelepiped_eq_convexHull, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, lowerSemicontinuousWithinAt_biSup, OrdinalApprox.le_lfpApprox, PrimeSpectrum.localization_comap_range, IsLocalization.orderIsoOfPrime_apply_coe, ConvexOn.inf_le_of_mem_convexHull, lowerSemicontinuousAt_biSup, VitaliFamily.FineSubfamilyOn.covering_disjoint, fixedPoints.ωSup_iterate_le_fixedPoint, absConvexHull_eq_empty, Matroid.IsBasis'.contract_dep_iff, Matroid.delete_indep_iff, FirstOrder.Language.Substructure.cg_iff_empty_or_exists_nat_generating_family, Disjoint.exists_thickenings, Matroid.Indep.disjoint_loops, AlgebraicGeometry.Scheme.propQCPrecoverage_monotone, MeasureTheory.hitting_eq_sInf, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, OrderHom.map_inf_fixedPoints_le, isClosed_closedAbsConvexHull, OrderHom.omegaCompletePartialOrder_ωSup_coe, essSup_mono_measure', AffineIndependent.convexHull_inter, Urysohns.CU.disjoint_C_support_lim, convex_closedConvexHull, closure_subset_closedAbsConvexHull, IsLocalization.map_algebraMap_ne_top_iff_disjoint, AlgebraicGeometry.Scheme.codisjoint_zeroLocus, FirstOrder.Language.Hom.eqOn_closure, Prod.ωSupImpl_snd, HasCardinalLT.Set.isFiltered_of_aleph0_le, OrderHom.isFixedPt_gfp, Matroid.delete_isCircuit_iff, Set.Finite.convexHull_eq, OrderHom.isLeast_lfp_le, MeasureTheory.hittingAfter_anti, SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_notMem, Affine.Simplex.convexHull_eq_closedInterior, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, Set.ncard_strictMono, le_ωSup_of_le, isClosed_closedConvexHull, OrderHom.map_lfp_comp, OrderHom.lfp_le_map, NumberField.InfinitePlace.disjoint_isReal_isComplex, Vitali.exists_disjoint_covering_ae', fixedPoints.ωSup_iterate_mem_fixedPoint, Set.Finite.encard_strictMonoOn, AddSubgroup.pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero, Matroid.IsBasis'.contract_indep_iff, lowerSemicontinuousOn_iff_le_liminf, OrderHom.lfp_le_fixed, Dynamics.coverEntropyInfEntourage_monotone, balanced_absConvexHull, convexHull_subset_affineSpan, convexHull_eq_self, disjoint_closedBall_ball_iff, OrderHom.le_gfp, IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal, Scott.IsOpen.isUpperSet, balancedHull_convexHull_subseteq_absConvexHull, PiNat.exists_disjoint_cylinder, Algebra.gc, NumberField.mixedEmbedding.disjoint_negAt_plusPart, PMF.toMeasure_apply_eq_zero_iff, UpperSemicontinuous.limsup_le, convexHull_range_eq_exists_affineCombination, convexIndependent_iff_notMem_convexHull_diff, OrderHom.map_gfp_comp, Topology.RelCWComplex.disjoint_base_iUnion_openCell, ContinuousHom.map_ωSup', AddAction.IsBlock.vadd_eq_or_disjoint, FirstOrder.Language.Substructure.lift_card_closure_le, FirstOrder.Language.Substructure.closure_eq, FirstOrder.Language.Substructure.mem_closure_iff_of_isRelational, FirstOrder.Language.Substructure.closure_mono, lowerSemicontinuous_biSup, FirstOrder.Language.Substructure.closure_univ, AlgebraicGeometry.sourceLocalClosure.le, FirstOrder.Language.Substructure.closure_image, AbsConvex.absConvexHull_eq, isLUB_range_ωSup, closedConvexHull_isClosed, Topology.RelCWComplex.disjoint_interior_base_iUnion_closedCell, le_essInf_of_ae_le, OrderHom.map_le_gfp, Matroid.setOf_dep_eq, closedAbsConvexHull_closure_eq_closedAbsConvexHull, AlgebraicGeometry.Spec.map_app, Complex.rectangle_eq_convexHull, FirstOrder.Language.Substructure.cg_closure_singleton, convexHull_subset_closedConvexHull, FirstOrder.Language.Structure.fg_iff, FirstOrder.Language.Substructure.cg_closure, Dynamics.coverMincard_monotone_subset, Finset.centerMass_mem_convexHull_of_nonpos
«term_→𝒄_» 📖	CompOp	—
ωScottContinuous 📖	MathDef	35 math math: ωScottContinuous_iff_apply₂, ωScottContinuous.comp, ScottContinuous.ωScottContinuous, ContinuousHom.ωScottContinuous, Prod.ωScottContinuous_fst, ContinuousHom.ωScottContinuous_apply, ωScottContinuous.of_apply₂, Prod.ωScottContinuous_snd, ωScottContinuous_iff_map_ωSup_of_orderHom, ContinuousHom.ωScottContinuous.seq, ωScottContinuous_iff_monotone_map_ωSup, Pi.ωScottContinuous_uncurry, CompleteLattice.ωScottContinuous.iSup, ωScottContinuous.const, CompleteLattice.ωScottContinuous.sSup, CompleteLattice.ωScottContinuous.sup, CompleteLattice.ωScottContinuous.inf, ωScottContinuous.apply₂, Part.ωScottContinuous_toUnitMono, ωScottContinuous.fun_comp, Topology.IsScott.ωScottContinuous_iff_continuous, ωScottContinuous.id, ωScottContinuous.of_map_ωSup_of_orderHom, ωScottContinuous.fun_const, ωScottContinuous.of_monotone_map_ωSup, ContinuousHom.ωScottContinuous.map, CompleteLattice.ωScottContinuous.top, Pi.ωScottContinuous_curry, ωScottContinuous.apply, Pi.uncurry_curry_ωScottContinuous, Submodule.coe_scott_continuous, Prod.ωScottContinuous.prodMk, CompleteLattice.ωScottContinuous.bot, ωScottContinuous.fun_id, ContinuousHom.ωScottContinuous.bind
ωSup 📖	CompOp	34 math math: le_ωSup, ContinuousHom.ωSup_apply, ωSup_total, fixedPoints.ωSup_iterate_le_prefixedPoint, ContinuousHom.ωSup_apply_ωSup, OrderHom.ωSup_coe, ωScottContinuous.map_ωSup_of_orderHom, ωSup_le_iff, Prod.ωSup_zip, ωScottContinuous.map_ωSup, ωScottContinuous_iff_map_ωSup_of_orderHom, Part.mem_ωSup, ωSup_le, ωScottContinuous_iff_monotone_map_ωSup, isωSup_ωSup, ωScottContinuous.monotone_map_ωSup, Part.fix_eq_ωSup, ωSup_le_ωSup_of_le, ωScottContinuous.isLUB, ContinuousHom.ωSup_bind, Prod.ωSup_snd, ContinuousHom.ωSup_def, Prod.ωSupImpl_fst, ContinuousHom.continuous, Prod.ωSup_fst, fixedPoints.ωSup_iterate_le_fixedPoint, ωSup_eq_of_isLUB, Part.fix_eq_ωSup_of_ωScottContinuous, OrderHom.omegaCompletePartialOrder_ωSup_coe, Prod.ωSupImpl_snd, le_ωSup_of_le, fixedPoints.ωSup_iterate_mem_fixedPoint, ContinuousHom.map_ωSup', isLUB_range_ωSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instOrderHomClassContinuousHom 📖	mathematical	—	OrderHomClass ContinuousHom Preorder.toLE PartialOrder.toPreorder toPartialOrder instFunLikeContinuousHom	—	OrderHom.mono
isLUB_range_ωSup 📖	mathematical	—	IsLUB Preorder.toLE PartialOrder.toPreorder toPartialOrder Set.range DFunLike.coe Chain Chain.instFunLikeNat ωSup	—	le_ωSup ωSup_le
le_ωSup 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder toPartialOrder DFunLike.coe Chain Chain.instFunLikeNat ωSup	—	—
le_ωSup_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder toPartialOrder DFunLike.coe Chain Chain.instFunLikeNat	Preorder.toLE PartialOrder.toPreorder toPartialOrder ωSup	—	le_trans le_ωSup
ωScottContinuous_iff_apply₂ 📖	mathematical	—	ωScottContinuous instOmegaCompletePartialOrderForall	—	ωScottContinuous.apply₂ ωScottContinuous.of_apply₂
ωScottContinuous_iff_map_ωSup_of_orderHom 📖	mathematical	—	ωScottContinuous DFunLike.coe OrderHom PartialOrder.toPreorder toPartialOrder OrderHom.instFunLike ωSup Chain.map	—	ωScottContinuous_iff_monotone_map_ωSup OrderHom.monotone'
ωScottContinuous_iff_monotone_map_ωSup 📖	mathematical	—	ωScottContinuous Monotone PartialOrder.toPreorder toPartialOrder ωSup Chain.map	—	ωScottContinuous.monotone ωScottContinuous.map_ωSup Chain.map_coe Set.range_comp ωSup_eq_of_isLUB isLUB_range_ωSup
ωSup_eq_of_isLUB 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder toPartialOrder Set.range DFunLike.coe Chain Chain.instFunLikeNat	ωSup	—	le_antisymm_iff le_ωSup ωSup_le_iff
ωSup_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder toPartialOrder DFunLike.coe Chain Chain.instFunLikeNat	Preorder.toLE PartialOrder.toPreorder toPartialOrder ωSup	—	—
ωSup_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder toPartialOrder ωSup DFunLike.coe Chain Chain.instFunLikeNat	—	le_ωSup ωSup_le
ωSup_le_ωSup_of_le 📖	mathematical	Chain PartialOrder.toPreorder toPartialOrder Chain.instLE	Preorder.toLE PartialOrder.toPreorder toPartialOrder ωSup	—	ωSup_le le_trans le_ωSup
ωSup_total 📖	mathematical	Preorder.toLE PartialOrder.toPreorder toPartialOrder DFunLike.coe Chain Chain.instFunLikeNat	Preorder.toLE PartialOrder.toPreorder toPartialOrder ωSup	—	by_cases ωSup_le le_ωSup_of_le

OmegaCompletePartialOrder.Chain

Definitions

Name	Category	Theorems
instFunLikeNat 📖	CompOp	16 math math: OmegaCompletePartialOrder.le_ωSup, zip_coe, OmegaCompletePartialOrder.ωSup_le_iff, pair_zero, range_pair, OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge, directed, ext_iff, instOrderHomClassNat, OmegaCompletePartialOrder.ωScottContinuous.isLUB, Scott.isωSup_iff_isLUB, map_coe, OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge', isChain_range, pair_succ, OmegaCompletePartialOrder.isLUB_range_ωSup
instInhabited 📖	CompOp	—
instLE 📖	CompOp	1 math math: map_le_map
instMembership 📖	CompOp	6 math math: Part.Fix.approx_mem_approxChain, mem_map, Part.mem_ωSup, Part.mem_chain_of_mem_ωSup, exists_of_mem_map, mem_map_iff
map 📖	CompOp	22 math math: map_id, OmegaCompletePartialOrder.ContinuousHom.ωSup_apply, OmegaCompletePartialOrder.OrderHom.ωSup_coe, OmegaCompletePartialOrder.ωScottContinuous.map_ωSup_of_orderHom, mem_map, map_le_map, OmegaCompletePartialOrder.ωScottContinuous.map_ωSup, OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom, OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup, OmegaCompletePartialOrder.ωScottContinuous.monotone_map_ωSup, OmegaCompletePartialOrder.ωScottContinuous.isLUB, OmegaCompletePartialOrder.ContinuousHom.ωSup_bind, map_coe, Prod.ωSup_snd, Prod.ωSupImpl_fst, OmegaCompletePartialOrder.ContinuousHom.continuous, Prod.ωSup_fst, mem_map_iff, OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder_ωSup_coe, Prod.ωSupImpl_snd, OmegaCompletePartialOrder.ContinuousHom.map_ωSup', map_comp
pair 📖	CompOp	4 math math: pair_zip_pair, pair_zero, range_pair, pair_succ
zip 📖	CompOp	4 math math: pair_zip_pair, OmegaCompletePartialOrder.ContinuousHom.ωSup_apply_ωSup, zip_coe, Prod.ωSup_zip

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directed 📖	mathematical	—	Directed Preorder.toLE DFunLike.coe OmegaCompletePartialOrder.Chain instFunLikeNat	—	directedOn_range IsChain.directedOn instReflLe isChain_range
exists_of_mem_map 📖	mathematical	OmegaCompletePartialOrder.Chain instMembership map	OmegaCompletePartialOrder.Chain instMembership DFunLike.coe OrderHom OrderHom.instFunLike	—	—
ext 📖	—	DFunLike.coe OmegaCompletePartialOrder.Chain instFunLikeNat	—	—	DFunLike.ext'
ext_iff 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.Chain instFunLikeNat	—	ext
instOrderHomClassNat 📖	mathematical	—	OrderHomClass OmegaCompletePartialOrder.Chain Preorder.toLE instFunLikeNat	—	—
isChain_range 📖	mathematical	—	IsChain Preorder.toLE Set.range DFunLike.coe OmegaCompletePartialOrder.Chain instFunLikeNat	—	Monotone.isChain_range OrderHomClass.mono instOrderHomClassNat
map_coe 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.Chain instFunLikeNat map OrderHom OrderHom.instFunLike	—	—
map_comp 📖	mathematical	—	map OrderHom.comp	—	—
map_id 📖	mathematical	—	map OrderHom.id	—	OrderHom.comp_id
map_le_map 📖	mathematical	OrderHom Preorder.toLE OrderHom.instPreorder	OmegaCompletePartialOrder.Chain instLE map	—	—
mem_map 📖	mathematical	OmegaCompletePartialOrder.Chain instMembership	OmegaCompletePartialOrder.Chain instMembership map DFunLike.coe OrderHom OrderHom.instFunLike	—	—
mem_map_iff 📖	mathematical	—	OmegaCompletePartialOrder.Chain instMembership map DFunLike.coe OrderHom OrderHom.instFunLike	—	exists_of_mem_map mem_map
pair_succ 📖	mathematical	Preorder.toLE	DFunLike.coe OmegaCompletePartialOrder.Chain instFunLikeNat pair	—	—
pair_zero 📖	mathematical	Preorder.toLE	DFunLike.coe OmegaCompletePartialOrder.Chain instFunLikeNat pair	—	—
pair_zip_pair 📖	mathematical	Preorder.toLE	zip pair Prod.instPreorder Prod.instLE_mathlib Preorder.toLE Prod.le_def	—	Prod.le_def OrderHom.ext
range_pair 📖	mathematical	Preorder.toLE	Set.range DFunLike.coe OmegaCompletePartialOrder.Chain instFunLikeNat pair Set Set.instInsert Set.instSingletonSet	—	Set.ext
zip_coe 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.Chain Prod.instPreorder instFunLikeNat zip	—	—

OmegaCompletePartialOrder.ContinuousHom

Definitions

Name	Category	Theorems
bind 📖	CompOp	1 math math: bind_apply
comp 📖	CompOp	4 math math: comp_id, id_comp, comp_assoc, comp_apply
const 📖	CompOp	1 math math: const_apply
copy 📖	CompOp	1 math math: copy_apply
flip 📖	CompOp	1 math math: flip_apply
id 📖	CompOp	3 math math: comp_id, id_comp, id_apply
inst 📖	CompOp	3 math math: ωSup_apply_ωSup, Prod.apply_apply, ωSup_def
instInhabited 📖	CompOp	—
map 📖	CompOp	1 math math: map_apply
ofFun 📖	CompOp	1 math math: ofFun_apply
seq 📖	CompOp	1 math math: seq_apply
toMono 📖	CompOp	2 math math: ωSup_apply, toMono_coe
toOrderHom 📖	CompOp	3 math math: coe_toOrderHom, toOrderHom_eq_coe, map_ωSup'
ωSup 📖	CompOp	2 math math: ωSup_apply, ωSup_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_mono 📖	mathematical	OmegaCompletePartialOrder.ContinuousHom Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.instPartialOrderContinuousHom OmegaCompletePartialOrder.toPartialOrder	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	—	OrderHom.apply_mono OmegaCompletePartialOrder.instOrderHomClassContinuousHom
bind_apply 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom Part Part.omegaCompletePartialOrder OmegaCompletePartialOrder.instFunLikeContinuousHom bind Part.bind instOmegaCompletePartialOrderForall	—	—
coe_apply 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike OrderHomClass.toOrderHom OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom OmegaCompletePartialOrder.instOrderHomClassContinuousHom	—	OmegaCompletePartialOrder.instOrderHomClassContinuousHom
coe_inj 📖	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	—	—	DFunLike.ext'
coe_mk 📖	mathematical	OrderHom.toFun PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike	—	—
coe_toOrderHom 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike toOrderHom OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	—	—
comp_apply 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	—
congr_arg 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	—	—
congr_fun 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	—	DFunLike.congr_fun
const_apply 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom const	—	—
continuous 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHomClass.toOrderHom OmegaCompletePartialOrder.instOrderHomClassContinuousHom	—	OmegaCompletePartialOrder.ωScottContinuous.map_ωSup ωScottContinuous
copy_apply 📖	mathematical	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom copy	—	—
ext 📖	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	—	ext
flip_apply 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom instOmegaCompletePartialOrderForall OmegaCompletePartialOrder.instFunLikeContinuousHom flip	—	—
forall_forall_merge 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom OmegaCompletePartialOrder.Chain OmegaCompletePartialOrder.instPartialOrderContinuousHom OmegaCompletePartialOrder.Chain.instFunLikeNat	—	le_trans monotone OrderHom.monotone le_max_right le_max_left
forall_forall_merge' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom OmegaCompletePartialOrder.Chain OmegaCompletePartialOrder.instPartialOrderContinuousHom OmegaCompletePartialOrder.Chain.instFunLikeNat	—	forall_forall_merge
id_apply 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom id	—	—
id_comp 📖	mathematical	—	comp id	—	—
map_apply 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom Part Part.omegaCompletePartialOrder OmegaCompletePartialOrder.instFunLikeContinuousHom map Part.map	—	—
map_ωSup' 📖	mathematical	—	OrderHom.toFun PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder toOrderHom OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map	—	—
monotone 📖	mathematical	—	Monotone PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	—	OrderHom.monotone'
ofFun_apply 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom ofFun	—	—
seq_apply 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom Part Part.omegaCompletePartialOrder OmegaCompletePartialOrder.instFunLikeContinuousHom seq Part.instMonad	—	—
toMono_coe 📖	mathematical	—	DFunLike.coe OrderHom OmegaCompletePartialOrder.ContinuousHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OmegaCompletePartialOrder.instPartialOrderContinuousHom OrderHom.instPreorder OrderHom.instFunLike toMono OrderHomClass.toOrderHom OmegaCompletePartialOrder.instFunLikeContinuousHom OmegaCompletePartialOrder.instOrderHomClassContinuousHom	—	—
toOrderHom_eq_coe 📖	mathematical	—	toOrderHom OrderHomClass.toOrderHom OmegaCompletePartialOrder.ContinuousHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OmegaCompletePartialOrder.instFunLikeContinuousHom OmegaCompletePartialOrder.instOrderHomClassContinuousHom	—	—
ωScottContinuous 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	—	OmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom map_ωSup'
ωScottContinuous_apply 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous OmegaCompletePartialOrder.ContinuousHom inst	OmegaCompletePartialOrder.ωScottContinuous DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	—	OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup OrderHom.apply_mono OmegaCompletePartialOrder.ωScottContinuous.monotone OmegaCompletePartialOrder.ωScottContinuous.map_ωSup le_antisymm OmegaCompletePartialOrder.ωSup_le OmegaCompletePartialOrder.instOrderHomClassContinuousHom continuous OmegaCompletePartialOrder.le_ωSup_of_le apply_mono OrderHom.monotone le_sup_left le_sup_right monotone le_refl
ωSup_apply 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom ωSup OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instPreorder OmegaCompletePartialOrder.instPartialOrderContinuousHom OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder toMono OrderHom.apply	—	—
ωSup_apply_ωSup 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom OmegaCompletePartialOrder.ωSup inst Prod.instOmegaCompletePartialOrder Prod.apply OmegaCompletePartialOrder.Chain.zip PartialOrder.toPreorder OmegaCompletePartialOrder.instPartialOrderContinuousHom OmegaCompletePartialOrder.toPartialOrder	—	—
ωSup_bind 📖	mathematical	—	OmegaCompletePartialOrder.ωSup Part Part.omegaCompletePartialOrder OmegaCompletePartialOrder.Chain.map PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.partBind Part.instMonad instOmegaCompletePartialOrderForall	—	eq_of_forall_ge_iff OmegaCompletePartialOrder.ωSup_le OrderHom.mono le_max_right le_max_left OmegaCompletePartialOrder.le_ωSup
ωSup_def 📖	mathematical	—	OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.ContinuousHom inst ωSup	—	—

OmegaCompletePartialOrder.ContinuousHom.Prod

Definitions

Name	Category	Theorems
apply 📖	CompOp	2 math math: OmegaCompletePartialOrder.ContinuousHom.ωSup_apply_ωSup, apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_apply 📖	mathematical	—	DFunLike.coe OmegaCompletePartialOrder.ContinuousHom Prod.instOmegaCompletePartialOrder OmegaCompletePartialOrder.ContinuousHom.inst OmegaCompletePartialOrder.instFunLikeContinuousHom apply	—	—

OmegaCompletePartialOrder.ContinuousHom.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—

OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bind 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous Part Part.omegaCompletePartialOrder instOmegaCompletePartialOrderForall	OmegaCompletePartialOrder.ωScottContinuous Part Part.omegaCompletePartialOrder Part.instMonad	—	OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup Monotone.partBind OmegaCompletePartialOrder.ωScottContinuous.monotone OmegaCompletePartialOrder.ωScottContinuous.map_ωSup OmegaCompletePartialOrder.ContinuousHom.ωSup_bind
map 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous Part Part.omegaCompletePartialOrder	OmegaCompletePartialOrder.ωScottContinuous Part Part.omegaCompletePartialOrder Part.instMonad	—	map_eq_bind_pure_comp Part.instLawfulMonad bind OmegaCompletePartialOrder.ωScottContinuous.const
seq 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous Part Part.omegaCompletePartialOrder	OmegaCompletePartialOrder.ωScottContinuous Part Part.omegaCompletePartialOrder Part.instMonad	—	Part.instLawfulMonad bind OmegaCompletePartialOrder.ωScottContinuous.of_apply₂ map

OmegaCompletePartialOrder.OrderHom

Definitions

Name	Category	Theorems
omegaCompletePartialOrder 📖	CompOp	2 math math: OmegaCompletePartialOrder.ContinuousHom.ωSup_apply, omegaCompletePartialOrder_ωSup_coe
ωSup 📖	CompOp	1 math math: ωSup_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
omegaCompletePartialOrder_ωSup_coe 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike OmegaCompletePartialOrder.ωSup omegaCompletePartialOrder OmegaCompletePartialOrder.Chain.map OrderHom.instPreorder OrderHom.apply	—	—
ωSup_coe 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike ωSup OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map OrderHom.instPreorder OrderHom.apply	—	—

OmegaCompletePartialOrder.fixedPoints

Definitions

Name	Category	Theorems
iterateChain 📖	CompOp	3 math math: ωSup_iterate_le_prefixedPoint, ωSup_iterate_le_fixedPoint, ωSup_iterate_mem_fixedPoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ωSup_iterate_le_fixedPoint 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom Set Set.instMembership Function.fixedPoints	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OmegaCompletePartialOrder.ωSup iterateChain OrderHomClass.toOrderHom OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom OmegaCompletePartialOrder.instOrderHomClassContinuousHom	—	ωSup_iterate_le_prefixedPoint Eq.le Function.mem_fixedPoints
ωSup_iterate_le_prefixedPoint 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OmegaCompletePartialOrder.ωSup iterateChain OrderHomClass.toOrderHom OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom OmegaCompletePartialOrder.instOrderHomClassContinuousHom	—	OmegaCompletePartialOrder.ωSup_le OmegaCompletePartialOrder.instOrderHomClassContinuousHom Function.iterate_succ_apply' le_trans OmegaCompletePartialOrder.ContinuousHom.monotone
ωSup_iterate_mem_fixedPoint 📖	mathematical	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom	Set Set.instMembership Function.fixedPoints DFunLike.coe OmegaCompletePartialOrder.ContinuousHom OmegaCompletePartialOrder.instFunLikeContinuousHom OmegaCompletePartialOrder.ωSup iterateChain OrderHomClass.toOrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OmegaCompletePartialOrder.instOrderHomClassContinuousHom	—	OmegaCompletePartialOrder.instOrderHomClassContinuousHom Function.mem_fixedPoints Function.IsFixedPt.eq_1 OmegaCompletePartialOrder.ContinuousHom.continuous le_antisymm OmegaCompletePartialOrder.ωSup_le Function.iterate_succ_apply' OmegaCompletePartialOrder.le_ωSup le_trans

OmegaCompletePartialOrder.ωScottContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous instOmegaCompletePartialOrderForall	—	apply₂ id
apply₂ 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous instOmegaCompletePartialOrderForall	OmegaCompletePartialOrder.ωScottContinuous	—	of_monotone_map_ωSup monotone map_ωSup
comp 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous	OmegaCompletePartialOrder.ωScottContinuous	—	of_monotone_map_ωSup Monotone.comp monotone map_ωSup
const 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous	—	ScottContinuousOn.const
fun_comp 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous	OmegaCompletePartialOrder.ωScottContinuous	—	comp
fun_const 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous	—	const
fun_id 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous	—	id
id 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous	—	ScottContinuousOn.id
isLUB 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous	IsLUB Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder Set.range DFunLike.coe OmegaCompletePartialOrder.Chain OmegaCompletePartialOrder.Chain.instFunLikeNat OmegaCompletePartialOrder.Chain.map monotone OmegaCompletePartialOrder.ωSup	—	monotone Set.range_comp Set.range_nonempty IsChain.directedOn instReflLe OmegaCompletePartialOrder.Chain.isChain_range OmegaCompletePartialOrder.isLUB_range_ωSup
map_ωSup 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous	OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder monotone	—	OmegaCompletePartialOrder.ωSup_eq_of_isLUB monotone isLUB
map_ωSup_of_orderHom 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map	—	OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom
monotone 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous	Monotone PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder	—	ScottContinuousOn.monotone OmegaCompletePartialOrder.Chain.range_pair
monotone_map_ωSup 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous	Monotone PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map	—	OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup
of_apply₂ 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous	OmegaCompletePartialOrder.ωScottContinuous instOmegaCompletePartialOrderForall	—	of_monotone_map_ωSup monotone map_ωSup
of_map_ωSup_of_orderHom 📖	mathematical	DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map	OmegaCompletePartialOrder.ωScottContinuous DFunLike.coe OrderHom PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.instFunLike	—	OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom
of_monotone_map_ωSup 📖	mathematical	Monotone PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map	OmegaCompletePartialOrder.ωScottContinuous	—	OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup

Part

Definitions

Name	Category	Theorems
omegaCompletePartialOrder 📖	CompOp	11 math math: OmegaCompletePartialOrder.ContinuousHom.bind_apply, OmegaCompletePartialOrder.ContinuousHom.seq_apply, mem_ωSup, OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.seq, fix_eq_ωSup, ωScottContinuous_toUnitMono, OmegaCompletePartialOrder.ContinuousHom.ωSup_bind, OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.map, fix_eq_ωSup_of_ωScottContinuous, OmegaCompletePartialOrder.ContinuousHom.map_apply, OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.bind
ωSup 📖	CompOp	2 math math: ωSup_eq_none, ωSup_eq_some

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_chain 📖	—	Part OmegaCompletePartialOrder.Chain PartialOrder.toPreorder instPartialOrder OmegaCompletePartialOrder.Chain.instMembership some	—	—	le_total OrderHom.monotone eq_some_iff mem_unique
mem_chain_of_mem_ωSup 📖	mathematical	Part instMembership ωSup	Part OmegaCompletePartialOrder.Chain PartialOrder.toPreorder instPartialOrder OmegaCompletePartialOrder.Chain.instMembership some	—	eq_some_iff
mem_ωSup 📖	mathematical	—	Part instMembership OmegaCompletePartialOrder.ωSup omegaCompletePartialOrder OmegaCompletePartialOrder.Chain PartialOrder.toPreorder instPartialOrder OmegaCompletePartialOrder.Chain.instMembership some	—	mem_chain_of_mem_ωSup eq_of_chain
ωSup_eq_none 📖	mathematical	Part OmegaCompletePartialOrder.Chain PartialOrder.toPreorder instPartialOrder OmegaCompletePartialOrder.Chain.instMembership some	ωSup none	—	—
ωSup_eq_some 📖	mathematical	Part OmegaCompletePartialOrder.Chain PartialOrder.toPreorder instPartialOrder OmegaCompletePartialOrder.Chain.instMembership some	ωSup some	—	eq_of_chain

Prod

Definitions

Name	Category	Theorems
instOmegaCompletePartialOrder 📖	CompOp	8 math math: OmegaCompletePartialOrder.ContinuousHom.ωSup_apply_ωSup, ωSup_zip, ωScottContinuous_fst, ωScottContinuous_snd, OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply, ωSup_snd, ωSup_fst, ωScottContinuous.prodMk
ωSupImpl 📖	CompOp	2 math math: ωSupImpl_fst, ωSupImpl_snd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ωScottContinuous_fst 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous instOmegaCompletePartialOrder	—	ScottContinuousOn.fst
ωScottContinuous_snd 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous instOmegaCompletePartialOrder	—	ScottContinuousOn.snd
ωSupImpl_fst 📖	mathematical	—	ωSupImpl OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.fst	—	—
ωSupImpl_snd 📖	mathematical	—	ωSupImpl OmegaCompletePartialOrder.ωSup OmegaCompletePartialOrder.Chain.map instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.snd	—	—
ωSup_fst 📖	mathematical	—	OmegaCompletePartialOrder.ωSup instOmegaCompletePartialOrder OmegaCompletePartialOrder.Chain.map instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.fst	—	—
ωSup_snd 📖	mathematical	—	OmegaCompletePartialOrder.ωSup instOmegaCompletePartialOrder OmegaCompletePartialOrder.Chain.map instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OrderHom.snd	—	—
ωSup_zip 📖	mathematical	—	OmegaCompletePartialOrder.ωSup instOmegaCompletePartialOrder OmegaCompletePartialOrder.Chain.zip PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder	—	—

Prod.ωScottContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodMk 📖	mathematical	OmegaCompletePartialOrder.ωScottContinuous	OmegaCompletePartialOrder.ωScottContinuous Prod.instOmegaCompletePartialOrder	—	ScottContinuousOn.prodMk OmegaCompletePartialOrder.Chain.range_pair

ScottContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ωScottContinuous 📖	mathematical	ScottContinuous PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder	OmegaCompletePartialOrder.ωScottContinuous	—	scottContinuousOn

(root)

Definitions

Name	Category	Theorems
instOmegaCompletePartialOrderForall 📖	CompOp	12 math math: OmegaCompletePartialOrder.ωScottContinuous_iff_apply₂, OmegaCompletePartialOrder.ContinuousHom.bind_apply, OmegaCompletePartialOrder.ωScottContinuous.of_apply₂, Pi.ωScottContinuous_uncurry, Part.fix_eq_ωSup, OmegaCompletePartialOrder.ContinuousHom.flip_apply, Part.ωScottContinuous_toUnitMono, OmegaCompletePartialOrder.ContinuousHom.ωSup_bind, Pi.ωScottContinuous_curry, OmegaCompletePartialOrder.ωScottContinuous.apply, Pi.uncurry_curry_ωScottContinuous, Part.fix_eq_ωSup_of_ωScottContinuous

---

← Back to Index