Basic

📁 Source: Mathlib/Order/BoundedOrder/Basic.lean

Statistics

Metric	Count
Definitions instBoundedOrder, BoundedOrder, toOrderBot, toOrderTop, rec, rec, OrderBot, toBot, instBot, instBoundedOrder, instOrderBot, instOrderTop, instTop, OrderTop, toTop, instBotForall, instBoundedOrder, instOrderBot, instOrderTop, instTopForall, instBot, instBoundedOrder, instOrderBot, instOrderTop, instTop, boundedOrder, orderBot, orderTop, instBot, instBoundedOrder, instOrderBot, instOrderTop, instTop, botOrderOrNoBotOrder, topOrderOrNoTopOrder	35
Theorems instSubsingleton, eq_bot, eq_top, eq_bot, eq_top, bot_lt, lt_top, ne_bot, ne_top, bot_lt, bot_lt', lt_top, lt_top', bot_le, ext_bot, instSubsingleton, ofDual_bot, ofDual_eq_bot, ofDual_eq_top, ofDual_top, toDual_bot, toDual_eq_bot, toDual_eq_top, toDual_top, ext_top, instSubsingleton, le_top, bot_apply, bot_comp, bot_def, top_apply, top_comp, top_def, fst_bot, fst_top, snd_bot, snd_top, coe_bot, coe_eq_bot_iff, coe_eq_top_iff, coe_top, mk_bot, mk_eq_bot_iff, mk_eq_top_iff, mk_top, down_bot, down_top, up_bot, up_top, bot_eq_false, bot_le, bot_lt_iff_ne_bot, bot_lt_of_lt, bot_lt_top, bot_ne_top, bot_notMem_iff, bot_unique, dite_ne_bot, dite_ne_top, eq_bot_iff, eq_bot_mono, eq_bot_of_bot_eq_top, eq_bot_of_minimal, eq_bot_of_top_eq_bot, eq_bot_or_bot_lt, eq_top_iff, eq_top_mono, eq_top_of_bot_eq_top, eq_top_of_top_eq_bot, eq_top_or_lt_top, isBot_bot, isBot_iff_eq_bot, isMax_iff_eq_top, isMax_top, isMin_bot, isMin_iff_eq_bot, isTop_iff_eq_top, isTop_top, ite_ne_bot, ite_ne_top, le_bot_iff, le_top, lt_top_iff_ne_top, lt_top_of_lt, ne_bot_of_gt, ne_bot_of_le_ne_bot, ne_top_of_le_ne_top, ne_top_of_lt, not_bot_lt_iff, not_isBot_iff_ne_bot, not_isMax_bot, not_isMax_iff_ne_top, not_isMin_iff_ne_bot, not_isMin_top, not_isTop_iff_ne_top, not_lt_bot, not_lt_top_iff, not_top_lt, subsingleton_iff_bot_eq_top, subsingleton_iff_top_eq_bot, subsingleton_of_bot_eq_top, subsingleton_of_top_eq_bot, subsingleton_of_top_le_bot, top_eq_true, top_le_iff, top_ne_bot, top_notMem_iff, top_unique	108
Total	143

Bool

Definitions

Name	Category	Theorems
instBoundedOrder 📖	CompOp	1 math, 2 bridge math: instIsSimpleOrder bridge: bot_eq_false, top_eq_true

BoundedOrder

Definitions

Name	Category	Theorems
toOrderBot 📖	CompOp	655 math, 1 bridge math: Algebra.range_ofId, sInf_univ, CategoryTheory.sheafBotEquivalence_functor, Subalgebra.LinearDisjoint.inf_eq_bot, Submodule.rTensorOne_symm_apply, coinduced_bot, AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology, Concept.intent_bot, iSupIndep.injOn_iInf, IntermediateField.LinearDisjoint.iff_inf_eq_bot, MeasurableSpace.comap_const, MonoidHom.ker_transferSylow_disjoint, Submodule.comm_trans_lTensorOne, IntermediateField.coe_algebraMap_over_bot, Set.disjoint_or_nonempty_inter, RingCon.toCon_eq_bot, NonUnitalStarAlgebra.mem_bot, IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot, Algebra.adjoin_singleton_intCast, BoundedOrderHomClass.map_bot, IsCompl.inf_left_eq_bot_iff, MeasurableSpace.comap_bot, codisjoint_bot, SeminormedGroup.disjoint_nhds, IntermediateField.coe_bot, isSimpleOrder_iff_isAtom_top, Submodule.mulMap_one_right_eq, CompleteLattice.isCompactElement_finsetSup, MeasureTheory.Measure.mutuallySingular_tfae, iSupIndep.disjoint_biSup, IntermediateField.lift_insepDegree_bot', Filter.disjoint_comap_iff, NonUnitalAlgebra.coe_bot, Equiv.Perm.disjoint_of_disjoint_support, sSup_eq_bot, NonUnitalStarAlgebra.coe_bot, IsCompactlyGenerated.BooleanGenerators.isAtom, iSup_false, algebraicClosure.algebraicClosure_eq_bot, AffineSubspace.comap_bot, BoundedLatticeHom.coe_comp_sup_hom', Module.End.invtSubmodule.disjoint_mk_iff, bot_lt_iSup, Directed.disjoint_iSup_right, CategoryTheory.Presieve.isSheaf_bot, Set.disjoint_union_right, MeasurableSpace.generateFrom_empty, IsGaloisGroup.fixedPoints_top, RingCon.comap_bot, MeasureTheory.condLExp_bot', AddCommMonoid.primaryComponent.disjoint, IntermediateField.botEquiv_symm, Subalgebra.op_bot, IsModularLattice.exists_disjoint_and_sup_eq, LieModule.disjoint_genWeightSpaceOf, Filter.disjoint_cocompact_left, Finset.Nonempty.sup_eq_top_iff, disjoint_nhds_cocompact, Algebra.adjoin_singleton_algebraMap, IntermediateField.relfinrank_bot_right, Coheyting.boundary_top, LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot, InfiniteGalois.mem_bot_iff_fixed, ProbabilityTheory.condIndep_bot_left, LieAlgebra.IsSemisimple.booleanGenerators, Polynomial.IsSplittingField.splits_iff, Set.disjoint_singleton_right, Partition.bot_notMem, t1Space_iff_disjoint_nhds_pure, bot_lt_affineSpan, Filter.disjoint_principal_left, isSeparatedMap_iff_disjoint_nhds, StarSubalgebra.bot_toSubalgebra, iSupIndep.pairwiseDisjoint, Subfield.splits_bot, Algebra.toSubring_bot, Subalgebra.LinearDisjoint.inf_eq_bot_of_commute, sSup_empty, LieSubmodule.disjoint_toSubmodule, IntermediateField.adjoin_zero, Filter.disjoint_comap_iff_map', Subalgebra.algebra_isAlgebraic_bot_right, T25Space.t2_5, Subalgebra.comm_trans_rTensorBot, AffineSubspace.not_wSameSide_bot, AlgebraicGeometry.Scheme.bot_mem_precoverage, Complementeds.mk_bot, Subalgebra.algebra_isAlgebraic_bot_left_iff, AddCon.toSetoid_bot, Equiv.Perm.disjoint_closure_of_disjoint_support, DirectedOn.disjoint_sSup_left, TopologicalSpace.Closeds.coe_eq_empty, sSupIndep.pairwiseDisjoint, TopologicalSpace.NoetherianSpace.exists_finset_irreducible, Metric.disjoint_cobounded_nhdsSet, sSup_atoms_le_eq, bot_covBy_top, Set.Iic.isCompl_inf_inf_of_isCompl_of_le, sSupHom.coe_bot, disjoint_rootsOfUnity_of_coprime, IsIntegrallyClosedIn.integralClosure_eq_bot, integralClosure_idem, instIsAbelianGaloisSubtypeMemIntermediateFieldBot, CategoryTheory.Sieve.functorPullback_bot, Algebra.mem_bot, CategoryTheory.Sieve.generate_bot, Filter.HasBasis.disjoint_iff_right, induced_topology_pure, FirstOrder.Language.Substructure.small_bot, disjoint_top, WellFoundedGT.finite_ne_bot_of_iSupIndep, Set.disjoint_left, Set.disjoint_singleton_left, Set.disjoint_right, StarSubalgebra.mem_bot, IntermediateField.bot_toSubalgebra, Algebra.toSubmodule_bot, Algebra.map_bot, Subfield.mem_bot_iff_pow_eq_self, LatticeHom.withTopWithBot'_toFun, Subfield.isTotallyReal_bot, Metric.disjoint_nhds_cobounded, Filter.disjoint_atTop_principal_Iio, Finset.Icc_bot_top, Algebra.adjoin_singleton_zero, Prop.bot_eq_false, Finset.inf_sup, Algebra.coe_bot, Setoid.injective_iff_ker_bot, MeasureTheory.condLExp_bot, sSupHom.bot_apply, SSet.Subcomplex.instSubsingletonHomToSSetBot, Fintype.IsSimpleOrder.univ, isOpen_setOf_disjoint_nhds_nhds, LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff, Partition.pairwiseDisjoint, Set.disjoint_singleton, IsDedekindDomain.integer_empty, AffineSubspace.not_sSameSide_bot, eq_bot_of_isCompl_top, Subgroup.FG.finset_sup, Subalgebra.eq_bot_of_finrank_one, disjoint_nhds_nhds_iff_not_specializes, iSupIndep_pair, mem_codiscrete, continuous_bot, IntermediateField.LinearDisjoint.bot_left, FirstOrder.Language.Substructure.cg_bot, IntermediateField.isTotallyReal_bot, SeparatedNhds.disjoint_nhdsSet, disjoint_nhdsSet_principal, Disjoint.filter_principal, Subalgebra.lTensorBot_one_tmul, Projectivization.Subspace.span_empty, iSupIndep.supIndep', Subalgebra.mulMap_bot_left_eq, Finset.truncatedInf_union_of_notMem, iSupIndep.supIndep, BoundedLatticeHom.coe_comp_lattice_hom', AffineSubspace.bot_coe, IntermediateField.instFiniteSubtypeMemBot, AffineSubspace.parallel_bot_iff_eq_bot, Filter.disjoint_iff, essSup_const_bot, SeminormedAddGroup.disjoint_nhds_zero, Filter.not_nonneg_sub_iff, CompleteSublattice.bot_mem, isClosed_and_discrete_iff, r1Space_iff_inseparable_or_disjoint_nhds, CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup, IntermediateField.finrank_eq_one_iff, AddSubmonoid.disjoint_def', Filter.isAtom_pure, IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic, IntermediateField.insepDegree_bot', isCoatom_bot, Submonoid.FG.finset_sup, Filter.disjoint_atBot_atTop, AddSubgroup.disjoint_def, Set.Icc_bot_top, CategoryTheory.GrothendieckTopology.bot_covers, AffineSubspace.smul_bot, isDenseEmbedding_pure, TopologicalSpace.Opens.coe_eq_empty, NonUnitalAlgebra.toSubmodule_bot, Filter.disjoint_cofinite_right, BoundedLatticeHom.coe_comp_sup_hom, IsLindelof.disjoint_nhdsSet_left, Filter.disjoint_map, PrimeSpectrum.iInf_localization_eq_bot, IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one, IntermediateField.botContinuousSMul, Subalgebra.unop_bot, isComplemented_bot, AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, BoundedLatticeHom.coe_toSupBotHom, Filter.disjoint_cofinite_left, LieAlgebra.IsSemisimple.sSup_atoms_eq_top, isCompl_iff, Set.not_disjoint_iff_nonempty_inter, Algebra.bijective_algebraMap_iff, hnot_top, Subgroup.subgroupOf_eq_bot, IsCompact.disjoint_nhdsSet_left, SSet.instHasDimensionLTToSSetBotSubcomplex, CategoryTheory.MorphismProperty.bot_mem_precoverage, LieAlgebra.IsSimple.isAtom_top, IntermediateField.rank_adjoin_eq_one_iff, iSupIndep_def'', Set.disjoint_insert_left, sSup_diff_singleton_bot, IsLindelof.disjoint_nhdsSet_right, TopologicalSpace.Closeds.coe_bot, IntermediateField.adjoin_one, CategoryTheory.sheafBotEquivalence_inverse_map_val, OrdinalApprox.lfpApprox_ord_eq_lfp, TopologicalSpace.Opens.coe_finset_sup, Setoid.bot_def, CategoryTheory.Subfunctor.Subpresheaf.bot_obj, Subfield.bot_eq_of_zMod_algebra, ConvexCone.disjoint_hull_left_of_convex, LT.lt.eq_bot, Filter.not_disjoint_self_iff, Filter.disjoint_of_disjoint_of_mem, MeasurableSpace.measurableSet_bot_iff, Subfield.map_bot, Submodule.comm_trans_rTensorOne, CategoryTheory.sheafBotEquivalence_unitIso, IntermediateField.extendScalars_self, BoundedOrderHom.coe_comp_botHom, Finset.sup_eq_top_iff, hnot_bot, iSupIndep_def', Finset.inf_eq_bot_iff, CategoryTheory.sheafBotEquivalence_inverse_obj_val, Subfield.roots_X_pow_char_sub_X_bot, MeasureTheory.Measure.mutuallySingular_iff_disjoint, Submodule.lTensorOne'_tmul, Submodule.rTensorOne'_tmul_one, isAtomic_of_complementedLattice, Con.toSetoid_eq_bot, Subgroup.disjoint_def', MeasureTheory.condExp_bot, Submodule.rTensorOne'_tmul, separatedNhds_iff_disjoint, TopologicalSpace.Opens.mem_bot, disjoint_nhdsSet_nhdsSet, iSupIndep.injOn, Finset.truncatedInf_empty, MeasurableSpace.generateFrom_singleton_univ, Quantale.mul_bot, Filter.nonneg_sub_iff, IsLprojection.coe_bot, Set.setOf_bot, disjoint_nhds_atBot_iff, sSup_atoms_eq_top, Real.disjoint_residual_ae, IsCompl.isCoatom_iff_isAtom, Set.bot_eq_empty, CompleteLinearOrder.himp_bot, iSupIndep_ne_bot, RootPairing.invtRootSubmodule.eq_bot_iff, clusterPt_iff_not_disjoint, StarSubalgebra.coe_bot, UniformSpace.toTopologicalSpace_bot, CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_hom, IntermediateField.finrank_adjoin_eq_one_iff, IntermediateField.bot_eq_top_of_rank_adjoin_eq_one, sSup_eq_bot', Partition.bot_notMem', IntermediateField.finrank_bot, Subgroup.disjoint_def, isCoatom_iff_eq_bot, IsIntegrallyClosed.integralClosure_eq_bot, IsIntegrallyClosed.integralClosure_eq_bot_iff, IntermediateField.sepDegree_bot, AddQuantale.add_bot, Submodule.rTensorOne_tmul, IntermediateField.finInsepDegree_bot', Filter.HasBasis.disjoint_iff, IntermediateField.restrictScalars_bot_eq_self, IntermediateField.fg_bot, Filter.limsInf_top, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff, TopologicalSpace.Closeds.isAtom_iff, GroupTopology.toTopologicalSpace_bot, Order.krullDim_le_one_iff_of_boundedOrder, isAtomic_of_isCoatomic_of_complementedLattice_of_isModular, Algebra.adjoin_singleton_one, CompleteSublattice.coe_bot, IntermediateField.adjoin_empty, Field.Emb.Cardinal.eq_bot_of_not_nonempty, Set.not_disjoint_iff, IntermediateField.rank_bot, CommMonoid.primaryComponent.disjoint, Set.disjoint_iff_inter_eq_empty, iSup_eq_dif, separableClosure_inf_perfectClosure, t2Space_iff_disjoint_nhds, Subalgebra.rTensorBot_tmul_one, ConvexCone.disjoint_coe, CompletelyNormalSpace.completely_normal, MeasureTheory.Measure.mutuallySingular_iff_disjoint_ae, Filter.disjoint_principal_principal, Finset.sup_inf, BoundedLatticeHom.map_bot', Subfield.bot_eq_of_charZero, RegularSpace.regular, IsIntegrallyClosedIn.integralClosure_eq_bot_iff, IsPGroup.disjoint_of_ne, Finset.truncatedInf_singleton, sSupIndep.disjoint_sSup, IsCompl.inf_eq_bot, Set.disjoint_insert_right, Set.pairwiseDisjoint_nhds, Prop.disjoint_iff, Filter.disjoint_comap_iff_map, IntermediateField.bot_eq_top_iff_finrank_eq_one, IntermediateField.adjoin_eq_bot_iff, MeasureTheory.SimpleFunc.simpleFunc_bot', Submodule.rTensorOne_tmul_one, Finset.truncatedInf_sups_of_notMem, CategoryTheory.GrothendieckTopology.trivial_eq_bot, FirstOrder.Language.Substructure.closure_empty, Filter.limsup_bot, Filter.disjoint_pure_pure, IntermediateField.lift_sepDegree_bot', AffineSubspace.coe_eq_bot_iff, Finset.Nonempty.inf_eq_bot_iff, iSup₂_eq_bot, essSup_measure_zero, Algebra.adjoin_singleton_natCast, IntermediateField.LinearDisjoint.inf_eq_bot, FirstOrder.Language.Substructure.map_bot, Subalgebra.bot_eq_top_iff_finrank_eq_one, Subalgebra.mulMap_bot_right_eq, AddSubgroup.FG.finset_sup, CategoryTheory.Subfunctor.bot_obj, R1Space.specializes_or_disjoint_nhds, iSupIndep.sup_indep_univ, Finset.sup_eq_iSup, Set.disjoint_univ, Subalgebra.lTensorBot_symm_apply, bot_codisjoint, disjoint_nhds_nhds_iff_not_inseparable, Con.toSetoid_bot, MeasureTheory.sigmaFinite_bot_iff, iSup_neg, disjoint_nhds_nhdsSet, IntermediateField.lift_bot, IsSimpleOrder.equivBool_symm_apply, LieSubmodule.instIsAtomicOfIsArtinian, IsGalois.fixedField_top, isSimpleOrder_iff, MulAction.BlockMem.coe_bot, Filter.not_one_le_div_iff, MeasureTheory.hittingAfter_eq_sInf, MeasureTheory.condLExp_bot_ae_eq, IsPGroup.le_or_disjoint_of_coprime, CategoryTheory.GrothendieckTopology.bot_covering, Submodule.mulMap_one_left_eq, AffineSubspace.isEmpty_bot, IntermediateField.adjoin_simple_eq_bot_iff, IntermediateField.relfinrank_bot_left, t1Space_iff_disjoint_pure_nhds, RingCon.matrix_bot, bot_lt_top, TopologicalSpace.Closeds.coe_finset_sup, TopologicalSpace.Opens.mk_empty, iSup_ne_bot_subtype, IntermediateField.adjoin_intCast, mem_codiscreteWithin, inf_sSup_eq_iSup_inf_sup_finset, Algebra.surjective_algebraMap_iff, IntermediateField.sepDegree_bot', CategoryTheory.Presheaf.isSheaf_bot, IntermediateField.LinearDisjoint.bot_right, Filter.limsSup_bot, AffineSubspace.pointwise_vadd_bot, iSup_emptyset, discreteTopology_bot, iSupIndep_def, RingCon.coe_bot, disjoint_pure_nhds, top_disjoint, IntermediateField.rank_eq_one_iff, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, Set.disjoint_iff_forall_ne, Subalgebra.fg_bot, IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable, Filter.disjoint_atTop_principal_Iic, AffineSubspace.not_sOppSide_bot, isSimpleOrder_iff_isCoatom_bot, disjoint_nhds_atTop, isAtomic_iff_isCoatomic, isDenseInducing_pure, eq_bot_of_top_isCompl, IntermediateField.isScalarTower_over_bot, ProbabilityTheory.condVar_bot', IntermediateField.bot_toSubfield, Metric.disjoint_cobounded_nhds, sSupIndep_pair, AffineSubspace.span_empty, NonUnitalStarAlgebra.map_bot, AffineSubspace.map_bot, Subalgebra.lTensorBot_tmul, NonUnitalAlgebra.adjoin_empty, Filter.HasBasis.disjoint_iff_left, Subgroup.isComplement'_iff_card_mul_and_disjoint, CategoryTheory.Sieve.functorPushforward_bot, disjoint_principal_nhdsSet, ProbabilityTheory.condIndep_bot_right, regularSpace_generateFrom, Order.Frame.himp_bot, mem_bot_iff_intCast, Filter.one_le_div_iff, IntermediateField.adjoin_natCast, BoundedLatticeHomClass.toSupBotHomClass, TopologicalSpace.Opens.coe_bot, IsCompactlyGenerated.BooleanGenerators.isAtomistic_of_sSup_eq_top, Complementeds.coe_bot, Set.univ_disjoint, TopologicalSpace.Closeds.isClopen_singleton_bot, IsCyclotomicExtension.singleton_one, MeasureTheory.hittingBtwn_eq_sInf, IntermediateField.isPurelyInseparable_bot, AddQuantale.bot_add, Filter.disjoint_atTop_atBot, SeminormedGroup.disjoint_nhds_one, AffineSubspace.map_eq_bot_iff, Filter.disjoint_prod, regularSpace_iff, Filter.disjoint_atBot_principal_Ioi, AddAction.BlockMem.coe_bot, Subalgebra.rTensorBot_symm_apply, RootPairing.coe_bot, ProbabilityTheory.indep_bot_right, ProbabilityTheory.condVar_bot_ae_eq, AffineSubspace.direction_bot, TopologicalSpace.Closeds.isAtom_coe, instIsAtomicFilter, AddSubgroup.disjoint_iff_add_eq_zero, MaximalSpectrum.iInf_localization_eq_bot, Set.disjoint_empty, Algebra.IsCentral.center_eq_bot, IsGaloisGroup.fixingSubgroup_bot, Finset.sup_eq_sSup_image, isAtomistic_of_complementedLattice, ProbabilityTheory.indep_bot_left, Partition.disjoint, Submodule.lTensorOne_symm_apply, BoundedOrderHomClass.toBotHomClass, IntermediateField.finInsepDegree_bot, MvPolynomial.supported_empty, LinearOrder.bot_topologicalSpace_eq_generateFrom, specializes_iff_not_disjoint, MeasureTheory.SimpleFunc.simpleFunc_bot, ConvexCone.disjoint_hull_right_of_convex, affineSpan_eq_bot, ProbabilityTheory.condVar_bot, fixedPoints.lfp_eq_sSup_iterate, Filter.limsup_const_bot, JacobsonNoether.exists_separable_and_not_isCentral', MeasureTheory.Measure.MutuallySingular.disjoint_ae, disjoint_nhds_pure, Submodule.lTensorOne'_one_tmul, IntermediateField.finrank_bot', sdiff_top, Quantale.bot_mul, isCompl_iff', CategoryTheory.Pretopology.toGrothendieck_bot, Partition.bot_lt_of_mem, Setoid.mk_eq_bot, Subalgebra.rank_eq_one_iff, DiscreteTopology.eq_bot, IntermediateField.botEquiv_def, Valuation.Integers.integralClosure, IntermediateField.finSepDegree_bot', disjoint_lift'_closure_nhds, stronglyMeasurable_bot_iff, IntermediateField.eq_bot_of_isSepClosed_of_isSeparable, IsSimpleOrder.lt_top_iff_eq_bot, WellFoundedLT.finite_ne_bot_of_iSupIndep, iSup_eq_if, FirstOrder.Language.Substructure.elementarySkolem₁Reduct.instSmall, TopologicalSpace.Opens.coe_disjoint, Subalgebra.eq_bot_of_rank_le_one, IntermediateField.bot_eq_top_of_finrank_adjoin_le_one, AddSubmonoid.disjoint_def, Submodule.lTensorOne_tmul, AddCon.toSetoid_eq_bot, IntermediateField.relrank_bot_right, AlgebraicGeometry.Scheme.IdealSheafData.support_top, Subalgebra.comm_trans_lTensorBot, InfiniteGalois.fixedField_bot, CompletelyDistribLattice.himp_bot, IsCompl.inf_right_eq_bot_iff, NonUnitalAlgebra.map_bot, IsSepClosed.separableClosure_eq_bot_iff, Subfield.closure_empty, Directed.disjoint_iSup_left, Subalgebra.bot_eq_top_of_finrank_eq_one, isAtom_iff_eq_top, isCompl_bot_top, Filter.disjoint_cocompact_right, AddSubgroup.disjoint_def', IsSimpleOrder.eq_bot_of_lt, complementedLattice_iff_isAtomistic, eq_bot_of_singletons_open, Subalgebra.isAlgebraic_bot_iff, Filter.disjoint_pure_atBot, isAtom_top, TwoSidedIdeal.bot_ringCon, r1Space_iff_specializes_or_disjoint_nhds, perfectClosure.eq_bot_of_isSeparable, subsingleton_iff_bot_eq_top, ProbabilityTheory.Kernel.indep_bot_left, MeasureTheory.sigmaFinite_trim_bot_iff, OrdinalApprox.lfp_mem_range_lfpApprox, Filter.compl_diagonal_mem_prod, IsCompactlyGenerated.BooleanGenerators.eq_atoms_of_sSup_eq_top, Partition.coe_removeBot, CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup, CompleteSublattice.disjoint_iff, BoundedLatticeHomClass.map_bot, subsingleton_iff_top_eq_bot, FirstOrder.Language.Substructure.instIsEmptySubtypeMemBotOfConstants, IntermediateField.insepDegree_bot, IsAlgClosed.algebraicClosure_eq_bot_iff, IntermediateField.rank_bot', iSupIndep_iff_supIndep, CompleteLattice.isAtomistic_iff, Filter.blimsup_false, MeasureTheory.condExp_bot', IsGalois.tfae, Subfield.card_bot, iSupIndep_iff_supIndep_univ, Finset.sup_univ_eq_iSup, IntermediateField.LinearDisjoint.eq_bot_of_self, ProbabilityTheory.Kernel.indep_bot_right, separableClosure.separableClosure_eq_bot, IsCompl.isAtom_iff_isCoatom, Submonoid.disjoint_def', NonUnitalAlgebra.mem_bot, pairwise_disjoint_nhds, Submodule.lTensorOne_one_tmul, iSup_of_empty, disjoint_nhds_atTop_iff, CategoryTheory.sheafBotEquivalence_counitIso, MeasureTheory.Measure.MutuallySingular.disjoint, IsCompact.disjoint_nhdsSet_right, AddSubgroup.addSubgroupOf_eq_bot, LieAlgebra.InvariantForm.atomistic, AffineSubspace.not_wOppSide_bot, Filter.HasBasis.disjoint_cobounded_iff, Representation.invtSubmodule.coe_bot, Filter.disjoint_atBot_principal_Ici, isCompl_top_bot, Metric.disjoint_nhdsSet_cobounded, Subfield.extendScalars_self, iSup_eq_bot, disjoint_nhdsSet_nhds, IntermediateField.relrank_bot_left, CompleteBooleanAlgebra.inf_compl_le_bot, Subalgebra.LinearDisjoint.eq_bot_of_commute_of_self, AddSubmonoid.FG.finset_sup, LieAlgebra.IsSemisimple.sSupIndep_isAtom, Subalgebra.finrank_bot, Submonoid.disjoint_def, Subgroup.disjoint_iff_mul_eq_one, Module.End.invtSubmodule.mk_eq_bot_iff, ZMod.fieldRange_castHom_eq_bot, IsSimpleOrder.bot_lt_iff_eq_top, AffineSubspace.eq_bot_or_nonempty, Filter.disjoint_pure_atTop, MeasureTheory.hitting_eq_sInf, IntermediateField.mem_bot, IsCompl.disjoint, Algebra.IsCentral.out, IsSimpleOrder.eq_bot_or_eq_top, SeminormedAddGroup.disjoint_nhds, IsCompl.le_left_iff, IsCompact.disjoint_nhdsSet_nhds, IsModularLattice.complementedLattice_Iic, Finset.sup_id_eq_sSup, IsSimpleOrder.instIsAtomic, IntermediateField.fixingSubgroup_bot, Set.disjoint_range_iff, Finset.exists_sup_eq_iSup, Subalgebra.bot_eq_top_iff_rank_eq_one, isGalois_bot, Subalgebra.rTensorBot_tmul, iSup_extend_bot, sSupHomClass.toSupBotHomClass, iSup_bot, Set.empty_disjoint, isGalois_iff_isGalois_bot, DirectedOn.disjoint_sSup_right, eq_sSup_atoms, LieAlgebra.IsSimple.isAtom_iff_eq_top, AffineSubspace.bot_parallel_iff_eq_bot, Set.disjoint_union_left, FirstOrder.Language.Substructure.fg_bot, Specializes.not_disjoint, IntermediateField.finrank_adjoin_simple_eq_one_iff, CompleteLattice.ωScottContinuous.bot, Subalgebra.LinearDisjoint.eq_bot_of_self, Module.End.invtSubmodule.disjoint_iff, separableClosure.eq_bot_iff, Subalgebra.LinearDisjoint.bot_left, Subalgebra.rank_bot, Coheyting.boundary_bot, Subalgebra.LinearDisjoint.bot_right, IntermediateField.rank_adjoin_simple_eq_one_iff, Concept.extent_bot, IsCompl.disjoint_right_iff, disjoint_nhds_atBot, MonoidHom.noncommCoprod_injective, notMem_iff_exists_ne_and_isConjRoot, LieIdeal.comap_incl_eq_bot, Algebra.adjoin_empty, Subalgebra.fg_bot_toSubmodule, Algebra.botEquiv_symm_apply, MeasurableSpace.generateFrom_singleton_empty, NonUnitalStarAlgebra.toNonUnitalSubalgebra_bot, BoundedOrderHom.map_bot', AffineSubspace.notMem_bot, IsCompl.disjoint_left_iff, Complementeds.disjoint_coe, DistribLattice.mem_ideal_sup_principal, MeasureTheory.condExp_bot_ae_eq, Subalgebra.bot_eq_top_of_rank_eq_one, RingCon.toCon_bot, IsGalois.mem_bot_iff_fixed, Subalgebra.finrank_eq_one_iff, IntermediateField.map_bot, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot, Subgroup.IsComplement'.disjoint, Set.disjoint_iff, Ultrafilter.isAtom, IsSimpleOrder.instIsAtomistic, disjoint_nhds_nhds, separableClosure.eq_bot_of_isPurelyInseparable, Subalgebra.eq_bot_of_isPurelyInseparable_of_isSeparable, IsCompl.le_right_iff, Set.Nonempty.not_disjoint, Subalgebra.finite_bot, IntermediateField.finSepDegree_bot, Filter.disjoint_principal_right, AddGroupTopology.toTopologicalSpace_bot, IsGaloisGroup.fixedPoints_eq_bot, LieModule.disjoint_genWeightSpace, Finset.truncatedInf_of_notMem, SSet.skeleton_zero, Ultrafilter.disjoint_iff_not_le bridge: bot_eq_false
toOrderTop 📖	CompOp	858 math, 1 bridge math: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top_iff, IsCyclotomicExtension.adjoin_primitive_root_eq_top, NonUnitalSubalgebra.center_eq_top, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.toPartialMap_hom, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, IntermediateField.finInsepDegree_top, OrderIso.map_radical, SSet.Subcomplex.preimage_eq_top_iff, measurable_from_top, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, IntermediateField.adjoin_eq_top_iff_of_isAlgebraic, Heyting.isRegular_top, IsCompl.sup_eq_top, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, TopologicalSpace.Opens.mem_top, AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.isAffineOpen_top, Finset.truncatedSup_infs, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, MeasureTheory.Measure.sub_top, BoundedOrderHomClass.map_top, eq_sInf_coatoms, Subalgebra.pi_top, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, sSup_univ, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, MeasureTheory.OuterMeasure.mkMetric_top, codisjoint_bot, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero, AffineBasis.tot, Algebra.mem_top, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, Filter.liminf_const_top, Finset.Colex.toColex_univ, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, IsOpen.exists_subset_affineIndependent_span_eq_top, SSet.iSup_subcomplexOfSimplex_prod_eq_top, isSimpleOrder_iff_isAtom_top, OrdinalApprox.gfp_mem_range_gfpApprox, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, AlgebraicGeometry.Scheme.Opens.topIso_inv, Opens.pretopology_toGrothendieck, CategoryTheory.Sieve.mem_iff_pullback_eq_top, iInf_of_empty, inseparable_top, Prop.codisjoint_iff, TensorAlgebra.adjoin_range_ι, NonUnitalStarAlgebra.mem_top, AlgHom.equalizer_eq_top, Subgroup.isCoatom_map, iInf_false, AlgebraicGeometry.Scheme.Hom.id_appTop, CategoryTheory.Presheaf.imageSieve_app, iInf_eq_top, IsGaloisGroup.fixingSubgroup_top, AddSubgroup.map_eq_range_iff, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, Algebra.toSubsemiring_eq_top, MeasureTheory.OuterMeasure.trim_top, RootPairing.invtRootSubmodule.eq_top_iff, IsLocalRing.closedPoint_mem_iff, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, QuotientAddGroup.leftRel_eq_top, TopologicalSpace.Opens.isCoatom_iff, Finset.Nonempty.sup_eq_top_iff, RingCon.matrix_top, SSet.Subcomplex.range_eq_top, AlgHom.fieldRange_eq_map, Field.exists_primitive_element, isGalois_iff_isGalois_top, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.Scheme.ι_toIso_inv, LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot, CategoryTheory.Subfunctor.range_toRange, UnitAddTorus.mFourierSubalgebra_closure_eq_top, Frm.Iso.mk_hom, Algebra.toSubring_eq_top, AddCon.toSetoid_top, NumberField.adjoin_eq_top_of_infinitePlace_lt, Polynomial.IsSplittingField.splits_iff, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, SSet.Subcomplex.topIso_inv_app_coe, polynomialFunctions.starClosure_topologicalClosure, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, CategoryTheory.GrothendieckTopology.trivial_covering, AffineEquiv.span_eq_top_iff, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, AffineSubspace.direction_eq_top_iff_of_nonempty, induced_const, affineSpan_singleton_union_vadd_eq_top_of_span_eq_top, integralClosure_eq_top_iff, interior_convexHull_nonempty_iff_affineSpan_eq_top, CompleteSublattice.top_mem, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, TopologicalSpace.eq_top_iff_forall_inseparable, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.PresheafedSpace.Γ_obj_op, IntermediateField.adjoin_univ, Finset.inf_id_eq_sInf, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, TopCat.GlueData.MkCore.V_id, AffineSubspace.linear_topEquiv, UniformSpace.toTopologicalSpace_top, CategoryTheory.Subfunctor.Subpresheaf.preimage_eq_top_iff, CategoryTheory.Sieve.top_apply, MulAction.BlockMem.coe_top, Algebra.EssFiniteType.adjoin_mem_finset, IsCompl.left_le_iff, AlgebraicGeometry.Scheme.Hom.preimage_top, Polynomial.IsSplittingField.adjoin_rootSet, IsModularLattice.complementedLattice_Ici, AlgebraicGeometry.Scheme.isoSpec_hom, AlgebraicGeometry.Scheme.ι_toIso_inv_assoc, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, NonUnitalSubalgebra.prod_top, AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, MeasurableSpace.map_const, bot_covBy_top, NonUnitalStarAlgebra.coe_top, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, Sublocale.top_mem, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, Subalgebra.center_eq_top, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, SSet.iSup_skeleton, PrimeSpectrum.iSup_basicOpen_eq_top_iff, IsNormalClosure.adjoin_rootSet, AffineBasis.tot', TopologicalSpace.Opens.isOpenEmbedding_obj_top, AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, SSet.Subcomplex.eq_top_iff_of_hasDimensionLT, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, iInf₂_eq_top, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc, disjoint_top, alternatingGroup.isCoatom_stabilizer_singleton, essInf_measure_zero, Polynomial.SplittingFieldAux.adjoin_rootSet, RingCon.subsingleton_quotient, CategoryTheory.Sieve.generate_top, SSet.Subcomplex.topIso_inv_ι, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top, IntermediateField.fixingSubgroup_top, AffineSubspace.coe_eq_univ_iff, CategoryTheory.Sieve.equalizer_self, TopologicalSpace.Opens.mk_univ, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, LatticeHom.withTopWithBot'_toFun, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, PMF.toOuterMeasure_caratheodory, IntermediateField.relfinrank_top_right, IndiscreteTopology.eq_top, Finset.Icc_bot_top, Finset.inf_sup, AlgebraicGeometry.Scheme.Hom.toPartialMap_domain, CompleteLinearOrder.top_sdiff, Submodule.toConvexCone_top, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.Γ_obj, CategoryTheory.Presieve.isSheafFor_top_sieve, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, SSet.hasDimensionLT_subcomplex_top_iff, IntermediateField.restrictScalars_top, Fintype.IsSimpleOrder.univ, EuclideanGeometry.Sphere.orthRadius_center, Representation.invtSubmodule.coe_top, Finset.top_eq_univ, TopologicalSpace.isOpen_top_iff, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.preimage_basicOpen_top, MvPolynomial.adjoin_range_X, AlgebraicGeometry.Scheme.ΓSpecIso_inv, NonUnitalAlgebra.range_id, IntermediateField.mem_top, AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, Field.primitive_element_iff_algHom_eq_of_eval', CategoryTheory.GrothendieckTopology.top_mem, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', adjoin_eq_top_of_conductor_eq_top, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, IntermediateField.relrank_top_right, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, Algebra.coe_top, TopologicalSpace.Opens.inclusion'_top_functor, MeasureTheory.Measure.mkMetric_top, Set.instNonemptyTop, SSet.Subcomplex.eq_top_iff_contains_nonDegenerate, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, Subalgebra.unop_top, AlgebraicGeometry.PresheafedSpace.Γ_map_op, AlgebraicGeometry.Scheme.id_appTop, sSup_compact_eq_top, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, BoundedLatticeHom.coe_comp_lattice_hom', Convex.interior_nonempty_iff_affineSpan_eq_top, Polynomial.adjoin_rootSet_eq_range, CategoryTheory.Presheaf.equalizerSieve_self_eq_top, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, TopCat.Presheaf.map_germ_eq_Γgerm, Algebra.top_toSubmodule, SSet.Subcomplex.preimage_range, AlgebraicGeometry.Scheme.ker_of_isAffine, Subalgebra.fg_of_submodule_fg, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, CliffordAlgebra.adjoin_range_ι, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, Finset.codisjoint_left, Polynomial.Splits.adjoin_rootSet_eq_range, Setoid.top_def, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, IntermediateField.lift_top, AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.tilde.isoTop_hom, CategoryTheory.Subfunctor.range_eq_top, borel_eq_top_of_discrete, isCoatom_bot, MulAction.isCoatom_stabilizer_iff_preprimitive, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, CategoryTheory.Subfunctor.Subpresheaf.image_top, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous, AlgebraicGeometry.Γ_restrict_isLocalization, IntermediateField.restrictScalars_eq_top_iff, Set.Icc_bot_top, Complementeds.coe_top, CategoryTheory.top_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, Opens.pretopology_ofGrothendieck, AlgebraicGeometry.ΓSpecIso_obj_hom, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one, Setoid.mk_eq_top, MeasureTheory.OuterMeasure.comap_top, CategoryTheory.Sieve.overEquiv_top, ProbabilityTheory.iIndep_comap_mem_iff, Field.exists_primitive_element_of_finite_bot, CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem, TopologicalSpace.Opens.functor_obj_map_obj, CategoryTheory.Sieve.arrows_eq_top_iff, Complementeds.codisjoint_coe, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, CategoryTheory.Sieve.arrows_top, Frm.Iso.mk_inv, QuotientAddGroup.rightRel_eq_top, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, isCompl_iff, AffineSubspace.mem_top, Algebra.bijective_algebraMap_iff, Subalgebra.topEquiv_apply, CategoryTheory.topologyOfClosureOperator_sieves, Field.exists_primitive_element_of_finite_top, IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic, continuous_top, MulAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, essInf_const_top, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AddGroupTopology.toTopologicalSpace_top, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, IntermediateField.rank_top, CompleteDistribLattice.top_sdiff, CategoryTheory.Sieve.generate_of_singleton_isSplitEpi, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, CategoryTheory.Sieve.functorPullback_top, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, NonUnitalAlgebra.top_toNonUnitalSubsemiring, Quotient.subsingleton_iff, PowerBasis.adjoin_gen_eq_top, BoundedLatticeHom.map_top', StarSubalgebra.eq_top_iff, Finset.Colex.ofColex_top, IntermediateField.adjoin_root_eq_top, AffineSubspace.smul_top, ConvexCone.toPointedCone_top, iInf_ne_top_subtype, CategoryTheory.GrothendieckTopology.discrete_eq_top, TopCat.Presheaf.map_germ_eq_Γgerm_assoc, NonUnitalStarAlgebra.top_toNonUnitalSubalgebra, Set.addCentralizer_empty, MeasureTheory.OuterMeasure.zero_caratheodory, ConvexCone.mem_top, IsLprojection.coe_top, MeasureTheory.OuterMeasure.top_caratheodory, TopologicalSpace.Closeds.coe_finset_inf, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, IntermediateField.finrank_top, Finset.sup_eq_top_iff, CompleteSublattice.codisjoint_iff, NonUnitalStarAlgebra.range_eq_top, separableClosure.eq_top_iff, Finset.inf_eq_bot_iff, ProbabilityTheory.iIndepSet.iIndep_comap_mem, Algebra.top_toSubring, AlgebraicGeometry.ΓSpec.left_triangle, CategoryTheory.Subfunctor.eq_top_iff_isIso, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, AlgebraicGeometry.AffineSpace.comp_homOfVector, IntermediateField.top_toSubalgebra, IntermediateField.relrank_top_left, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, AlgebraicGeometry.Scheme.homOfLE_appTop, IsGaloisGroup.fixedPoints_bot, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, nhds_top, AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom, exists_root_adjoin_eq_top_of_isCyclic, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.Scheme.isoSpec_Spec_hom, AddMonoid.Coprod.codisjoint_mrange_inl_mrange_inr, sSup_atoms_eq_top, IntermediateField.finrank_eq_one_iff_eq_top, SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, IsCompl.isCoatom_iff_isAtom, TopologicalSpace.Opens.coe_finset_inf, AlgebraicGeometry.tilde.isIso_toOpen_top, Subfield.extendScalars_top, AlgebraicGeometry.HasRingHomProperty.appTop, AffineSubspace.mk'_top, Algebra.zariskisMainProperty_iff_exists_saturation_eq_top, NumberField.is_primitive_element_of_infinitePlace_lt, CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top, MonoidAlgebra.exists_finset_adjoin_eq_top, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, IntermediateField.bot_eq_top_of_rank_adjoin_eq_one, SeparationQuotient.inseparableSetoid_eq_top_iff, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, AddSubgroup.codisjoint_addSubgroupOf_sup, PowerBasis.adjoin_eq_top_of_gen_mem_adjoin, isCoatom_iff_eq_bot, NonUnitalAlgebra.eq_top_iff, AlgebraicGeometry.SheafedSpace.Γ_map, Polynomial.IsSplittingField.adjoin_rootSet', AlgebraicGeometry.germ_stalkClosedPointIso_hom, IsCompl.right_le_iff, ProbabilityTheory.Kernel.iIndep_comap_mem_iff, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, OrdinalApprox.gfpApprox_ord_eq_gfp, CategoryTheory.Coverage.eq_top_pullback, BoundedOrderHom.coe_comp_topHom, AlgebraicGeometry.Scheme.toIso_inv_ι_assoc, AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, AlgebraicGeometry.Scheme.toSpecΓ_appTop, Order.Coframe.top_sdiff, CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top', Order.krullDim_le_one_iff_of_boundedOrder, Finset.codisjoint_right, AlgHom.range_eq_top, CategoryTheory.Subfunctor.Subpresheaf.epi_iff_range_eq_top, NonUnitalAlgebra.mem_top, Set.top_eq_univ, NonUnitalStarAlgebra.toNonUnitalSubalgebra_eq_top, SSet.Subcomplex.image_top, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty, AffineSubspace.topEquiv_symm_apply_coe, FrameHom.coe_toInfTopHom, AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective, Module.End.invtSubmodule.mk_eq_top_iff, TopologicalSpace.Opens.inclusion'_map_eq_top, Subalgebra.centralizer_eq_top_iff_subset, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, MeasureTheory.Measure.add_top, Heyting.Regular.coe_top, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, Algebra.top_toSubsemiring, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, AlgebraicGeometry.Scheme.Opens.ι_appTop, AddMonoid.Coprod.codisjoint_range_inl_range_inr, Finset.sup_inf, AffineMap.map_top_of_surjective, AlgebraicGeometry.Scheme.map_basicOpen, CategoryTheory.Subfunctor.Subpresheaf.top_obj, NonUnitalAlgebra.adjoin_univ, AlgebraicGeometry.isRetrocompact_basicOpen, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, IntermediateField.bot_eq_top_iff_finrank_eq_one, FrameHom.map_sSup', AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, CategoryTheory.Sieve.pullback_eq_top_of_mem, AlgebraicGeometry.Scheme.comp_appTop_assoc, AlgebraicGeometry.Proj.basicOpen_one, CompleteLattice.isCoatomistic_iff, CompletelyDistribLattice.top_sdiff, Subalgebra.op_top, AlgebraicGeometry.Scheme.isoSpec_Spec, CategoryTheory.Subfunctor.Subpresheaf.range_id, Finset.Nonempty.inf_eq_bot_iff, Field.exists_primitive_element_iff_finite_intermediateField, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, Field.Emb.Cardinal.filtration_apply, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, indiscreteTopology_iff, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, Subalgebra.bot_eq_top_iff_finrank_eq_one, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, AddMonoidAlgebra.exists_finset_adjoin_eq_top, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, CategoryTheory.Subfunctor.instIsIsoFunctorTypeιTop, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.SheafedSpace.Γ_obj_op, Algebra.isAlgebraic_iff, TopologicalSpace.Closeds.coe_top, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, NonUnitalStarAlgebra.comap_top, bot_codisjoint, FreeAlgebra.adjoin_range_ι, ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, SSet.Subcomplex.topIso_inv_ι_assoc, AlgebraicGeometry.Scheme.inv_appTop, IntermediateField.finrank_top', AlgebraicGeometry.isLocalization_away_of_isAffine, Finset.map_truncatedSup, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AffineSubspace.direction_top, Affine.Simplex.span_eq_top, IsSimpleOrder.equivBool_symm_apply, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, WithBot.sInf_empty, TopologicalSpace.Opens.eq_bot_or_top, AlgebraicGeometry.morphismRestrict_appTop, isSimpleOrder_iff, IsLocalRing.closed_point_mem_iff, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, Algebra.IsAlgebraic.isNormalClosure_iff, iInf_top, AlgebraicGeometry.Scheme.Hom.preimage_opensRange, StarSubalgebra.toSubalgebra_eq_top, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, StarSubalgebra.mem_top, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, CategoryTheory.GrothendieckTopology.bot_covering, AlgebraicGeometry.LocallyRingedSpace.Γ_map, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, exists_subset_affineIndependent_affineSpan_eq_top, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, bot_lt_top, Algebra.adjoin_adjoin_coe_preimage, AlgebraicGeometry.eq_top_of_sigmaSpec_subset_of_isCompact, Algebra.adjoin_top, FrameHomClass.toInfTopHomClass, AlgebraicGeometry.PresheafedSpace.Γ_obj, AffineSubspace.perpBisector_eq_top, Algebra.adjoin_root_eq_top_of_isSplittingField, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, Algebra.surjective_algebraMap_iff, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, Field.primitive_element_iff_minpoly_degree_eq, Algebra.toSubmodule_eq_top, AlgHom.fieldRange_eq_top, Subgroup.map_eq_range_iff, DualNumber.range_inlAlgHom_sup_adjoin_eps, AlgebraicGeometry.Scheme.toOpen_eq, isPurelyInseparable_iff_perfectClosure_eq_top, top_disjoint, BoundedLatticeHomClass.map_top, bot_himp, Algebra.adjoin_univ, AlgHom.equalizer_same, CategoryTheory.Subfunctor.image_top, TopologicalSpace.Closeds.coe_eq_univ, AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one, IntermediateField.adjoin_root_eq_top_of_isSplittingField, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, algebraicClosure.eq_top_iff, isSimpleOrder_iff_isCoatom_bot, AddAction.BlockMem.coe_top, IsOpen.exists_between_affineIndependent_span_eq_top, Setoid.eq_top_iff, AffineSubspace.top_coe, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, Field.primitive_element_iff_minpoly_natDegree_eq, isAtomic_iff_isCoatomic, sInfHom.coe_top, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, Subalgebra.fg_top, NonUnitalAlgebra.toSubmodule_eq_top, AlgebraicGeometry.Scheme.Hom.inv_appTop, SSet.iSup_skeletonOfMono, affineSpan_coe_preimage_eq_top, AffineSubspace.pointwise_vadd_top, Complementeds.mk_top, TwoSidedIdeal.top_ringCon, AffineSubspace.perpBisector_self, Module.End.invtSubmodule.codisjoint_iff, AlgebraicGeometry.Spec_zeroLocus, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, IntermediateField.topEquiv_symm_apply_coe, affineSpan_eq_top_of_nonempty_interior, SSet.iSup_range_eq_top_of_isColimit, IntermediateField.rank_top', Subalgebra.topEquiv_symm_apply_coe, AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app, MeasureTheory.OuterMeasure.boundedBy_top, AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective, iInf_eq_dif, CompleteSublattice.coe_top, IntermediateField.topEquiv_apply, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AffineSubspace.topEquiv_apply, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem, iInf_extend_top, IsCyclotomicExtension.singleton_one, MeasureTheory.hittingBtwn_eq_sInf, SSet.finite_subcomplex_top_iff, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, Algebra.adjoin_restrictScalars, alternatingGroup.isCoatom_stabilizer, NonUnitalAlgebra.coe_top, QuotientGroup.rightRel_eq_top, NonUnitalAlgebra.map_top, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.Scheme.topIso_hom, MeasurableSpace.generateFrom_singleton, AlgebraicGeometry.finite_appTop_of_universallyClosed, AffineSubspace.span_univ, IntermediateField.top_toSubfield, TopologicalSpace.IsOpenCover.iSup_eq_top, NonUnitalAlgebra.to_subring_eq_top, eq_top_of_bot_isCompl, RingOfIntegers.exponent_eq_one_iff, AlgebraicGeometry.specTargetImageFactorization_app_injective, Algebra.comap_top, AlgebraicGeometry.PresheafedSpace.Γ_map, NonUnitalAlgebra.toNonUnitalSubring_eq_top, IsSimpleOrder.instIsCoatomistic, AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective, CategoryTheory.Sieve.functorInclusion_top_isIso, CompleteBooleanAlgebra.top_le_sup_compl, AffineBasis.isUnit_toMatrix_iff, Set.exists_seq_iSup_eq_top_iff_countable, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, sInfHomClass.toInfTopHomClass, AffineSubspace.instNonemptySubtypeMemTop, AlgebraicGeometry.affineAnd_apply, Concept.intent_top, IntermediateField.fg_top, instDiscreteMeasurableSpace, MeasureTheory.OuterMeasure.top_apply', AlgebraicGeometry.AffineSpace.reindex_appTop_coord, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, IsCyclotomicExtension.iff_adjoin_eq_top, AlgEquiv.fieldRange_eq_top, Equiv.Perm.isCoatom_stabilizer, Field.Emb.Cardinal.iSup_adjoin_eq_top, AlgebraicGeometry.ΓSpec.toSpecΓ_of, sInf_diff_singleton_top, Set.centralizer_empty, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, AlgebraicGeometry.IsAffine.affine, StarSubalgebra.coe_top, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, AlgebraicGeometry.SheafedSpace.Γ_obj, AlgebraicGeometry.Scheme.mem_basicOpen_top, ConvexCone.isGenerating_top, LieSubmodule.codisjoint_toSubmodule, isCompl_iff', AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, Algebra.eq_top_iff, Filter.liminf_bot, AffineSubspace.comap_top, fourierSubalgebra_closure_eq_top, Filter.limsInf_bot, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, NonUnitalStarAlgebra.range_id, Subalgebra.prod_top, CategoryTheory.Sieve.overEquiv_symm_top, NonUnitalAlgebra.comap_top, MeasureTheory.Measure.toOuterMeasure_top, NonUnitalStarAlgebra.map_top, AlgebraicGeometry.Scheme.comp_appTop, Finset.inf_eq_sInf_image, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, subalgebra_top_finrank_eq_submodule_top_finrank, IntermediateField.adjoin_eq_top_iff, Finset.inf_eq_iInf, IsCyclotomicExtension.Rat.adjoin_singleton_eq_top, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, AlgebraicGeometry.isField_of_universallyClosed, polynomialFunctions.topologicalClosure, sInf_empty, RingCon.range_mkₐ, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, compl_top, IsSimpleOrder.lt_top_iff_eq_bot, MeasurableSpace.map_top, RootPairing.coe_top, Algebra.map_top, Concept.extent_top, CategoryTheory.Subfunctor.top_obj, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top, CategoryTheory.Sieve.functorPushforward_top, NonUnitalStarSubalgebra.center_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_top, IntermediateField.bot_eq_top_of_finrank_adjoin_le_one, CategoryTheory.Presieve.isSeparatedFor_top, BoundedOrderHomClass.toTopHomClass, Subgroup.codisjoint_subgroupOf_sup, AlgebraicGeometry.Scheme.map_basicOpen_map, CompleteLattice.ωScottContinuous.top, BoundedLatticeHom.coe_toInfTopHom, StarAlgHom.range_eq_map_top, AlgebraicGeometry.Scheme.Hom.comp_appTop, NonUnitalStarAlgebra.eq_top_iff, Subalgebra.bot_eq_top_of_finrank_eq_one, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, RingCon.toCon_eq_top, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, MeasureTheory.OuterMeasure.map_top_of_surjective, isAtom_iff_eq_top, SemidirectProduct.mulEquivSubgroup_apply, isCompl_bot_top, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, MvPolynomial.supported_univ, conductor_eq_top_iff_adjoin_eq_top, fixedPoints.gfp_eq_sInf_iterate, isAtom_top, AdjoinRoot.adjoinRoot_eq_top, AlgebraicGeometry.Scheme.IsLocallyDirected.V_self, borel_eq_top_of_countable, CategoryTheory.GrothendieckTopology.top_mem', TopCat.Presheaf.Γgerm_res_apply, IntermediateField.extendScalars_top, subsingleton_iff_bot_eq_top, ConvexCone.coe_top, MeasurableSpace.measurableSet_top, CategoryTheory.Presheaf.equalizerSieve_eq_top_iff, IntermediateField.fixedField_bot, NonUnitalAlgebra.range_eq_top, SemidirectProduct.mulEquivSubgroup_symm_apply, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen, Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl, AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, FrameHom.toFun_eq_coe, AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, Complex.adjoin_I, SSet.Subcomplex.range_eq_top_iff, Con.toSetoid_top, AlgebraicGeometry.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, Finset.exists_inf_eq_iInf, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, ContinuousMap.elemental_id_eq_top, Opens.toPretopology_grothendieckTopology, MeasureTheory.OuterMeasure.map_top, Algebra.FiniteType.out, subsingleton_iff_top_eq_bot, polynomialFunctions_closure_eq_top', Finset.inf_univ_eq_iInf, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial, Projectivization.Subspace.span_univ, AlgebraicGeometry.Scheme.toIso_inv_ι, IsSimpleOrder.eq_top_of_lt, OpenSubgroup.toOpens_top, eq_top_of_isCompl_bot, iInf_eq_if, TopologicalSpace.Opens.map_top, CategoryTheory.Functor.imageSieve_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, CategoryTheory.Sieve.pullback_top, Set.not_top_subset, IntermediateField.insepDegree_top, ProjectiveSpectrum.basicOpen_one, BoundedLatticeHom.coe_comp_inf_hom', AlgebraicGeometry.Scheme.Γevaluation_naturality, RingCon.coe_top, OpenAddSubgroup.toOpens_top, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, CategoryTheory.Sieve.uliftFunctorInclusion_top_isIso, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, NonUnitalStarSubalgebra.prod_top, IsCompl.codisjoint, AlgebraicGeometry.Spec.fromSpecStalk_eq, IsCompl.isAtom_iff_isCoatom, NonUnitalAlgebra.top_toSubring, ContinuousMapZero.elemental_eq_top, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, IntermediateField.fg_top_iff, CategoryTheory.GrothendieckTopology.top_covers, CategoryTheory.Presieve.factorsThru_top, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', induced_top, AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq, IntermediateField.relfinrank_top_left, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, BoundedLatticeHom.coe_comp_inf_hom, sInf_eq_top, iInf_neg, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, Finset.truncatedSup_infs_of_notMem, GroupTopology.toTopologicalSpace_top, iInf_lt_top, Con.toSetoid_eq_top, MeasureTheory.OuterMeasure.dirac_caratheodory, IntermediateField.finSepDegree_top, SSet.N.iSup_subcomplex_eq_top, IsOpen.affineSpan_eq_top, CategoryTheory.Sieve.id_mem_iff_eq_top, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, IsAdjoinRoot.primitive_element_root, Monoid.Coprod.codisjoint_range_inl_range_inr, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, AlgebraicGeometry.Scheme.Opens.ι_image_top, BoundedLatticeHomClass.toInfTopHomClass, isCompl_top_bot, Field.Emb.Cardinal.adjoin_basis_eq_top, NonUnitalAlgebra.top_toSubmodule, Algebra.TensorProduct.adjoin_tmul_eq_top, AlgebraicGeometry.Scheme.Γ_obj_op, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints, SSet.Subcomplex.topIso_hom, CategoryTheory.Sieve.pullback_ofObjects_eq_top, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, AlgebraicGeometry.Scheme.Opens.topIso_hom, MeasureTheory.OuterMeasure.top_apply, CategoryTheory.presheafIsGeneratedBy_of_isFinite, IsSimpleOrder.bot_lt_iff_eq_top, Subalgebra.restrictScalars_top, QuotientGroup.leftRel_eq_top, PrimeSpectrum.basicOpen_one, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, MeasureTheory.Measure.top_add, AlgebraicGeometry.AffineSpace.map_appTop_coord, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, PrimeSpectrum.iSup_basicOpen_eq_top_iff', Filter.bliminf_false, MeasureTheory.hitting_eq_sInf, AlgebraicGeometry.isIso_fromTildeΓ_iff, AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv, polynomialFunctions_closure_eq_top, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, IsSimpleOrder.eq_bot_or_eq_top, IsDedekindDomain.integer_univ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, LT.lt.eq_top, IsAdjoinRoot.adjoin_root_eq_top, NonUnitalAlgebra.toNonUnitalSubring_top, iInf_emptyset, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, CategoryTheory.PreOneHypercover.sieve₀_trivial, CategoryTheory.Subfunctor.preimage_eq_top_iff, Module.End.invtSubmodule.codisjoint_mk_iff, CategoryTheory.Subfunctor.Subpresheaf.eq_top_iff_isIso, CategoryTheory.Presieve.isSheafFor_top, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, Subalgebra.bot_eq_top_iff_rank_eq_one, IntermediateField.coe_top, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, Algebra.range_id, Polynomial.SplittingField.adjoin_rootSet, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, isSplittingField_iff_intermediateField, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, IsModularLattice.exists_inf_eq_and_codisjoint, TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr, Polynomial.adjoin_X, TopologicalSpace.Opens.coe_top, isCoatomic_of_isAtomic_of_complementedLattice_of_isModular, CategoryTheory.Subfunctor.epi_iff_range_eq_top, CategoryTheory.PreOneHypercover.sieve₁_trivial, StarSubalgebra.top_toSubalgebra, BoundedOrderHom.map_top', Monoid.Coprod.codisjoint_mrange_inl_mrange_inr, IsSimpleOrder.equivBool_apply, CategoryTheory.Subfunctor.Subpresheaf.range_eq_top, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, instIndiscreteTopology, NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top, TopologicalSpace.Opens.coe_eq_univ, Field.primitive_element_iff_algHom_eq_of_eval, Set.setOf_top, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, CategoryTheory.Subfunctor.range_id, separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable, ContinuousMap.idealOfSet_isMaximal_iff, AddCon.toSetoid_eq_top, AlgebraicGeometry.instIsAffineHomιBasicOpen, compl_bot, AddAction.isCoatom_stabilizer_iff_preprimitive, AddAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive, CategoryTheory.Sieve.generate_of_contains_isSplitEpi, Subalgebra.rank_top, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, Subalgebra.bot_eq_top_of_rank_eq_one, sInfHom.top_apply, CategoryTheory.Subfunctor.Subpresheaf.range_toRange, AlgebraicGeometry.SheafedSpace.restrictTopIso_hom, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, MeasureTheory.OuterMeasure.toMeasure_top, Prop.top_eq_true, IsSimpleOrder.instIsCoatomic, subalgebra_top_rank_eq_submodule_top_rank, isComplemented_top, AlgebraicGeometry.SheafedSpace.Γ_map_op, RingCon.toCon_top, isCyclic_tfae, affineSpan_eq_top_iff_nonempty_of_subsingleton, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, CategoryTheory.GrothendieckTopology.top_covering, alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl, Filter.limsSup_top, AlgebraicGeometry.LocallyRingedSpace.Γ_obj, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, IntermediateField.sepDegree_top, Subgroup.isCoatom_comap, AlgebraicGeometry.Scheme.toSpecΓ_base bridge: top_eq_true

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSubsingleton 📖	mathematical	—	BoundedOrder Preorder.toLE PartialOrder.toPreorder	—	OrderTop.instSubsingleton OrderBot.instSubsingleton

IsBot

Definitions

Name	Category	Theorems
rec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_bot 📖	mathematical	IsBot Preorder.toLE PartialOrder.toPreorder	Bot.bot OrderBot.toBot	—	isBot_iff_eq_bot

IsMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_top 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder	Top.top OrderTop.toTop	—	isMax_iff_eq_top

IsMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_bot 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder	Bot.bot OrderBot.toBot	—	isMin_iff_eq_bot

IsTop

Definitions

Name	Category	Theorems
rec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_top 📖	mathematical	IsTop Preorder.toLE PartialOrder.toPreorder	Top.top OrderTop.toTop	—	isTop_iff_eq_top

LT.lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_lt 📖	mathematical	Preorder.toLT	Bot.bot OrderBot.toBot Preorder.toLE	—	bot_lt_of_lt
lt_top 📖	mathematical	Preorder.toLT	Top.top OrderTop.toTop Preorder.toLE	—	lt_top_of_lt
ne_bot 📖	—	Preorder.toLT	—	—	ne_bot_of_gt
ne_top 📖	—	Preorder.toLT	—	—	ne_top_of_lt

Ne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Bot.bot OrderBot.toBot Preorder.toLE	—	bot_lt_iff_ne_bot
bot_lt' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Bot.bot OrderBot.toBot Preorder.toLE	—	bot_lt
lt_top 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Top.top OrderTop.toTop Preorder.toLE	—	lt_top_iff_ne_top
lt_top' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Top.top OrderTop.toTop Preorder.toLE	—	lt_top

OrderBot

Definitions

Name	Category	Theorems
toBot 📖	CompOp	827 math, 1 bridge math: Finset.bot_eq_empty, le_bot_iff, Algebra.range_ofId, sInf_univ, PNat.bot_eq_one, CategoryTheory.sheafBotEquivalence_functor, Subalgebra.LinearDisjoint.inf_eq_bot, Set.Ici.coe_bot, Submodule.rTensorOne_symm_apply, IsAtom.lt_iff, coinduced_bot, AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology, Finset.Ico_bot, Finpartition.empty_parts, YoungDiagram.cells_bot, min_eq_bot, Concept.intent_bot, iSupIndep.injOn_iInf, IntermediateField.LinearDisjoint.iff_inf_eq_bot, MeasurableSpace.comap_const, nhds_bot_basis, PrimeSpectrum.asIdeal_bot, Disjoint.le_bot, partialSups_succ', Submodule.comm_trans_lTensorOne, IntermediateField.coe_algebraMap_over_bot, RingCon.toCon_eq_bot, NonUnitalStarAlgebra.mem_bot, IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot, grade_bot, Seminorm.bot_eq_zero, lt_compl_self, Additive.ofMul_bot, Algebra.adjoin_singleton_intCast, BoundedOrderHomClass.map_bot, BotHom.bot_apply, min_bot_left, IsCompl.inf_left_eq_bot_iff, AddMonoidAlgebra.supDegree_single, MeasurableSpace.comap_bot, codisjoint_bot, ProperCone.innerDual_univ, DiscreteQuotient.proj_bot_inj, WithBot.subtypeOrderIso_symm_apply, List.foldr_max_of_ne_nil, MeasureTheory.hittingAfter_bot_le_iff, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.Scheme.Hom.preimage_bot, IntermediateField.coe_bot, Submodule.mulMap_one_right_eq, bot_sdiff, IntermediateField.lift_insepDegree_bot', Disjoint.eq_bot_of_ge, NonUnitalAlgebra.coe_bot, bot_lt_of_lt, sSup_eq_bot, NonUnitalStarAlgebra.coe_bot, IsCompl.bihimp_eq_bot, iSup_false, algebraicClosure.algebraicClosure_eq_bot, AffineSubspace.comap_bot, PUnit.bot_eq, BoundedLatticeHom.coe_comp_sup_hom', Finsupp.bot_eq_zero, bot_lt_iSup, Multiset.sup_zero, CategoryTheory.Presieve.isSheaf_bot, MeasurableSpace.generateFrom_empty, Set.accumulate_bot, IsGaloisGroup.fixedPoints_top, RingCon.comap_bot, MeasureTheory.condLExp_bot', CategoryTheory.Functor.WellOrderInductionData.Extension.map_zero, IsLowerSet.bot_mem, IntermediateField.botEquiv_symm, Subalgebra.op_bot, YoungDiagram.coe_bot, Algebra.adjoin_singleton_algebraMap, CategoryTheory.TransfiniteCompositionOfShape.fac_assoc, IntermediateField.relfinrank_bot_right, Coheyting.boundary_top, LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot, AlgebraicGeometry.Scheme.IdealSheafData.radical_bot, InfiniteGalois.mem_bot_iff_fixed, ProbabilityTheory.condIndep_bot_left, CategoryTheory.Functor.WellOrderInductionData.surjective, InnerProductSpace.gramSchmidt_bot, Polynomial.IsSplittingField.splits_iff, Partition.bot_notMem, himp_bot, bot_lt_affineSpan, StarSubalgebra.bot_toSubalgebra, LowerSet.Iio_bot, SemilatInfCat_dual_comp_forget_to_partOrd, BotHom.dual_apply_apply, Icc_isBoundaryPoint_bot, Subfield.splits_bot, Algebra.toSubring_bot, partialSups_add_one', PrincipalSeg.map_bot, Subalgebra.LinearDisjoint.inf_eq_bot_of_commute, CategoryTheory.Functor.WellOrderInductionData.sectionsMk_val_op_bot, sSup_empty, IntermediateField.adjoin_zero, IsBot.eq_bot, IsAtomic.eq_bot_or_exists_atom_le, Subalgebra.algebra_isAlgebraic_bot_right, CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot, BoxIntegral.Prepartition.IsPartition.compl_eq_bot, SemilatSupCat.Iso.mk_inv_toFun, Subalgebra.comm_trans_rTensorBot, AffineSubspace.not_wSameSide_bot, AlgebraicGeometry.Scheme.bot_mem_precoverage, Finset.sup_erase_bot, Complementeds.mk_bot, Subalgebra.algebra_isAlgebraic_bot_left_iff, ContinuousMap.concatCM_left, CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_isoBot, AddCon.toSetoid_bot, Finset.Iio_eq_Ico, TopologicalSpace.Closeds.coe_eq_empty, max_bot_left, disjoint_bot_right, bot_covBy_top, ProperCone.coe_bot, Order.Ideal.principal_bot, sSupHom.coe_bot, isBot_iff_eq_bot, IsIntegrallyClosedIn.integralClosure_eq_bot, CategoryTheory.Subobject.bot_eq_initial_to, integralClosure_idem, ClosedSubmodule.mem_bot, Sum.Lex.inl_bot, instIsAbelianGaloisSubtypeMemIntermediateFieldBot, CategoryTheory.Sieve.functorPullback_bot, Algebra.mem_bot, WithTop.instOrderedSub, CategoryTheory.Sieve.generate_bot, induced_topology_pure, FirstOrder.Language.Substructure.small_bot, Multiplicative.ofAdd_eq_bot, disjoint_top, InitialSeg.map_bot, WellFoundedGT.finite_ne_bot_of_iSupIndep, Order.IsNormal.ext, GradeMinOrder.exists_nat_orderEmbedding_of_forall_covby_finite, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, StarSubalgebra.mem_bot, ENNReal.bot_eq_zero, IntermediateField.bot_toSubalgebra, Algebra.toSubmodule_bot, Algebra.map_bot, Subfield.mem_bot_iff_pow_eq_self, List.max_le_of_forall_le, Subfield.isTotallyReal_bot, IsAtom.bot_covBy, Fin.rev_top, AlgebraicGeometry.Scheme.IdealSheafData.zero_eq_bot, Finset.Icc_bot_top, Algebra.adjoin_singleton_zero, Prop.bot_eq_false, Algebra.coe_bot, Setoid.injective_iff_ker_bot, MeasureTheory.condLExp_bot, sSupHom.bot_apply, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot, Multiset.sup_coe, Filter.OrderBot.atBot_eq, SSet.Subcomplex.instSubsingletonHomToSSetBot, Fintype.IsSimpleOrder.univ, Nimber.bot_eq_zero, AlgebraicGeometry.isSchemeTheoreticallyDominant_iff, Finpartition.ofErase_parts, bot_symmDiff, NatOrdinal.bot_eq_zero, Flag.bot_mem, sdiff_self, IsDedekindDomain.integer_empty, AffineSubspace.not_sSameSide_bot, eq_bot_of_isCompl_top, Ordinal.bot_eq_zero, Subalgebra.eq_bot_of_finrank_one, IsPredArchimedean.pred_findAtom, MeasureTheory.hittingBtwn_bot_le_iff, continuous_bot, IntermediateField.LinearDisjoint.bot_left, FirstOrder.Language.Substructure.cg_bot, IntermediateField.isTotallyReal_bot, DiscreteQuotient.proj_bot_bijective, MeasureTheory.lowerCrossingTime_zero, compl_inf_eq_bot, BoxIntegral.Prepartition.compl_top, SupBotHom.bot_apply, Subalgebra.lTensorBot_one_tmul, WithBot.succ_eq_bot, Pairwise.disjoint_extend_bot, Projectivization.Subspace.span_empty, limsup_eq_bot, Subalgebra.mulMap_bot_left_eq, Finset.truncatedInf_union_of_notMem, OrderIsoClass.toSupBotHomClass, BoundedLatticeHom.coe_comp_lattice_hom', AffineSubspace.bot_coe, IntermediateField.instFiniteSubtypeMemBot, not_lt_bot, AffineSubspace.parallel_bot_iff_eq_bot, FractionalIdeal.absNorm_bot, CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, bot_sup_eq, ClosedSubmodule.bot_orthogonal_eq_top, essSup_const_bot, AlgebraicGeometry.Scheme.ker_toSpecΓ, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, WellFoundedLT.induction_bot, IsPredArchimedean.findAtom_eq_bot, CategoryTheory.Subobject.bot_factors_iff_zero, disjoint_iff, MonomialOrder.bot_eq_zero, CompleteSublattice.bot_mem, Directed.extend_bot, List.le_max_of_le, IntermediateField.finrank_eq_one_iff, Finpartition.parts_eq_empty_iff, AddMonoidAlgebra.supDegree_zero, BoxIntegral.Prepartition.bot_boxes, IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic, disjoint_bot_left, IntermediateField.insepDegree_bot', ClosedSubmodule.top_orthogonal_eq_bot, Set.Ico.coe_bot, isCoatom_bot, PrimeSpectrum.basicOpen_zero, Set.Icc_bot_top, CategoryTheory.GrothendieckTopology.bot_covers, AffineSubspace.smul_bot, isDenseEmbedding_pure, TopologicalSpace.Opens.coe_eq_empty, NonUnitalAlgebra.toSubmodule_bot, BoundedLatticeHom.coe_comp_sup_hom, not_supIrred_bot, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_bot, PrimeSpectrum.iInf_localization_eq_bot, IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one, Finset.sup_empty, IntermediateField.botContinuousSMul, Subalgebra.unop_bot, isComplemented_bot, AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, BoundedLatticeHom.coe_toSupBotHom, ProperCone.dual_univ, StrictMono.apply_eq_bot_iff, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le, Algebra.bijective_algebraMap_iff, Set.Iic.complementedLattice_iff, hnot_top, bot_lt_iff_ne_bot, SSet.instHasDimensionLTToSSetBotSubcomplex, CategoryTheory.MorphismProperty.bot_mem_precoverage, IntermediateField.rank_adjoin_eq_one_iff, CategoryTheory.TransfiniteCompositionOfShape.map_isoBot, sSup_diff_singleton_bot, Finset.Iic_bot, TopologicalSpace.Closeds.coe_bot, Order.not_isSuccLimit_bot, IntermediateField.adjoin_one, CategoryTheory.sheafBotEquivalence_inverse_map_val, OrdinalApprox.lfpApprox_ord_eq_lfp, ClosedSubmodule.coe_bot, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, LowerSet.Iio_eq_bot, CategoryTheory.TransfiniteCompositionOfShape.fac, Setoid.bot_def, CategoryTheory.Subfunctor.Subpresheaf.bot_obj, Subfield.bot_eq_of_zMod_algebra, NNReal.bot_eq_zero, LT.lt.eq_bot, SemilatSupCat.dual_map, CategoryTheory.Limits.imageSubobject_zero, Order.pred_bot, Finset.Iic_eq_Icc, MeasurableSpace.measurableSet_bot_iff, Subfield.map_bot, Submodule.comm_trans_rTensorOne, CategoryTheory.Subobject.map_bot, Disjoint.out, CategoryTheory.sheafBotEquivalence_unitIso, BoxIntegral.Prepartition.iUnion_eq_empty, MeasureTheory.Content.innerContent_bot, SimpleGraph.Finsubgraph.coe_bot, IntermediateField.extendScalars_self, BoundedOrderHom.coe_comp_botHom, Finpartition.default_eq_empty, hnot_bot, CategoryTheory.Subobject.mk_eq_bot_iff_zero, AlgebraicGeometry.Scheme.IdealSheafData.bot_mul, isAtomic_iff, le_compl_self, IsAtom.le_iff, csSup_empty, GaloisConnection.l_eq_bot, Finset.inf_eq_bot_iff, CategoryTheory.sheafBotEquivalence_inverse_obj_val, Subfield.roots_X_pow_char_sub_X_bot, Submodule.lTensorOne'_tmul, Disjoint.eq_bot_of_self, Submodule.rTensorOne'_tmul_one, Con.toSetoid_eq_bot, MeasureTheory.condExp_bot, Submodule.rTensorOne'_tmul, TopologicalSpace.Opens.mem_bot, MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp, iSupIndep.injOn, Seminorm.sSup_empty, Finset.truncatedInf_empty, Heyting.Regular.coe_bot, MeasurableSpace.generateFrom_singleton_univ, Quantale.mul_bot, IsLprojection.coe_bot, Set.setOf_bot, SupBotHom.coe_sup, Set.bot_eq_empty, CompleteLinearOrder.himp_bot, sup_eq_bot_iff, Multiset.bot_eq_zero, iSupIndep_ne_bot, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, FractionalIdeal.bot_eq_zero, RootPairing.invtRootSubmodule.eq_bot_iff, Set.Ioi_bot, eq_bot_or_bot_lt, StarSubalgebra.coe_bot, DFinsupp.bot_eq_zero, UniformSpace.toTopologicalSpace_bot, CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_hom, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, IntermediateField.finrank_adjoin_eq_one_iff, Nonneg.bot_eq, IntermediateField.bot_eq_top_of_rank_adjoin_eq_one, sSup_eq_bot', bot_eq_one', Multiplicative.toAdd_eq_bot, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, Finset.Ici_bot, Partition.bot_notMem', IntermediateField.finrank_bot, symmDiff_self, sdiff_sdiff_self, Order.isSuccPrelimit_bot, isCoatom_iff_eq_bot, IsIntegrallyClosed.integralClosure_eq_bot, IsIntegrallyClosed.integralClosure_eq_bot_iff, IntermediateField.sepDegree_bot, AlgebraicGeometry.Scheme.Hom.ker_eq_bot_of_isIso, bddLat_dual_comp_forget_to_semilatSupCat, AddQuantale.add_bot, Submodule.rTensorOne_tmul, StrictAnti.apply_eq_bot_iff, IntermediateField.finInsepDegree_bot', IntermediateField.restrictScalars_bot_eq_self, Disjoint.eq_bot_of_le, sup_bot_eq, BotHom.coe_bot, Additive.toMul_bot, IntermediateField.fg_bot, IccLeftChart_extend_bot, Filter.limsInf_top, AlgebraicGeometry.Scheme.nilradical_eq_bot, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff, GroupTopology.toTopologicalSpace_bot, Order.krullDim_le_one_iff_of_boundedOrder, Algebra.adjoin_singleton_one, transfiniteIterate_bot, CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot, CompleteSublattice.coe_bot, IntermediateField.adjoin_empty, BoxIntegral.Prepartition.iUnion_bot, ciSup_of_empty, OrderHom.bot_def, IsUpperSet.bot_mem, Fin.bot_eq_zero, Field.Emb.Cardinal.eq_bot_of_not_nonempty, IntermediateField.rank_bot, CategoryTheory.TransfiniteCompositionOfShape.iic_F, IsAtom.bot_lt, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w, iSup_eq_dif, Seminorm.coe_bot, separableClosure_inf_perfectClosure, Multiplicative.ofAdd_bot, inf_compl_self, Subalgebra.rTensorBot_tmul_one, sdiff_eq_bot_iff, Nucleus.coe_bot, WithBot.orderSucc_bot, MeasureTheory.hitting_bot_le_iff, BoundedLatticeHom.map_bot', Subfield.bot_eq_of_charZero, IsIntegrallyClosedIn.integralClosure_eq_bot_iff, Finset.truncatedInf_singleton, bddLat_dual_comp_forget_to_semilatInfCat, IsCompl.inf_eq_bot, IntermediateField.bot_eq_top_iff_finrank_eq_one, IntermediateField.adjoin_eq_bot_iff, MeasureTheory.SimpleFunc.simpleFunc_bot', Submodule.rTensorOne_tmul_one, Finset.truncatedInf_sups_of_notMem, CategoryTheory.GrothendieckTopology.trivial_eq_bot, FirstOrder.Language.Substructure.closure_empty, Filter.limsup_bot, IntermediateField.lift_sepDegree_bot', bot_le, OrderIsoClass.toBotHomClass, AffineSubspace.coe_eq_bot_iff, Finset.Nonempty.inf_eq_bot_iff, iSup₂_eq_bot, essSup_measure_zero, Algebra.adjoin_singleton_natCast, Finset.min_eq_bot, IntermediateField.LinearDisjoint.inf_eq_bot, SupBotHom.sup_apply, FirstOrder.Language.Substructure.map_bot, Subalgebra.bot_eq_top_iff_finrank_eq_one, Subalgebra.mulMap_bot_right_eq, BotHom.sup_apply, CategoryTheory.Subfunctor.bot_obj, Set.dissipate_bot, IsMin.eq_bot, Subalgebra.lTensorBot_symm_apply, MeasureTheory.upperCrossingTime_zero, bot_covBy_iff, bot_codisjoint, Pi.isAtom_iff_eq_single, Con.toSetoid_bot, max_eq_bot, ClosedSubmodule.orthogonal_eq_top_iff, MeasureTheory.sigmaFinite_bot_iff, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isoBot, iSup_neg, IntermediateField.lift_bot, Order.height_bot, IsSimpleOrder.equivBool_symm_apply, IsGalois.fixedField_top, InfHom.withBot'_toFun, TopologicalSpace.Opens.eq_bot_or_top, isSimpleOrder_iff, MulAction.BlockMem.coe_bot, ext_bot, MeasureTheory.hittingAfter_eq_sInf, MeasureTheory.condLExp_bot_ae_eq, CategoryTheory.GrothendieckTopology.bot_covering, SupHom.withBot'_toFun, Submodule.mulMap_one_left_eq, AffineSubspace.isEmpty_bot, IntermediateField.adjoin_simple_eq_bot_iff, IntermediateField.relfinrank_bot_left, LT.lt.bot_lt, CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape.mem_map_bot_le, AlgebraicGeometry.Scheme.Hom.ker_eq_bot, RingCon.matrix_bot, bot_lt_top, HeytingHomClass.map_bot, AlgebraicGeometry.Scheme.instIsIsoSubschemeιBotIdealSheafData, TopologicalSpace.Opens.mk_empty, iSup_ne_bot_subtype, IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top, IntermediateField.adjoin_intCast, Pi.isAtom_iff, Algebra.surjective_algebraMap_iff, IntermediateField.sepDegree_bot', ProperCone.toPointedCone_bot, CategoryTheory.Presheaf.isSheaf_bot, IntermediateField.LinearDisjoint.bot_right, Filter.limsSup_bot, Finset.sup_eq_bot_of_isEmpty, BoxIntegral.Prepartition.distortion_bot, AffineSubspace.pointwise_vadd_bot, CategoryTheory.Subobject.bot_arrow, IsAtom.Iic_eq, iSup_emptyset, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, discreteTopology_bot, BotHom.dual_symm_apply_apply, AlgebraicGeometry.Scheme.Hom.ker_toNormalization, WithBot.succ_bot, SemilatSupCat.Iso.mk_hom_toFun, compl_bihimp_self, RingCon.coe_bot, top_disjoint, IntermediateField.rank_eq_one_iff, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, bot_himp, ContDiffMapSupportedIn.seminorm_eq_bot_of_gt, Subalgebra.fg_bot, disjoint_of_le_iff_left_eq_bot, IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable, ClosedSubmodule.inf_orthogonal_eq_bot, ProjectiveSpectrum.basicOpen_zero, map_eq_bot_iff, AffineSubspace.not_sOppSide_bot, isSimpleOrder_iff_isCoatom_bot, IsMaxChain.bot_mem, LatticeHom.withBot'_toFun, Additive.ofMul_eq_bot, CategoryTheory.Subobject.bot_eq_zero, isDenseInducing_pure, symmDiff_eq_bot, eq_bot_of_top_isCompl, IntermediateField.isScalarTower_over_bot, ProbabilityTheory.condVar_bot', max_bot_right, bot_mem_lowerBounds, IntermediateField.bot_toSubfield, compl_inf_self, AffineSubspace.span_empty, WithBot.lt_coe_bot, NonUnitalStarAlgebra.map_bot, AffineSubspace.map_bot, Subalgebra.lTensorBot_tmul, NonUnitalAlgebra.adjoin_empty, TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal, CategoryTheory.Sieve.functorPushforward_bot, ProbabilityTheory.condIndep_bot_right, Order.Frame.himp_bot, mem_bot_iff_intCast, IntermediateField.adjoin_natCast, BoundedLatticeHomClass.toSupBotHomClass, TopologicalSpace.Opens.coe_bot, WithBot.subtypeOrderIso_apply_coe, Complementeds.coe_bot, Set.Iic_bot, AlgebraicGeometry.Scheme.IdealSheafData.comap_bot, TopologicalSpace.Closeds.isClopen_singleton_bot, IsCyclotomicExtension.singleton_one, MeasureTheory.hittingBtwn_eq_sInf, isMin_iff_eq_bot, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, IntermediateField.isPurelyInseparable_bot, AddQuantale.bot_add, Order.le_pred_iff_eq_bot, CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app, inf_bot_eq, AffineSubspace.map_eq_bot_iff, AddAction.BlockMem.coe_bot, Subalgebra.rTensorBot_symm_apply, RootPairing.coe_bot, IsAtom.ne_iff_eq_bot, ProbabilityTheory.indep_bot_right, Set.Icc.coe_bot, ProbabilityTheory.condVar_bot_ae_eq, AffineSubspace.direction_bot, FractionalIdeal.bot_lt_mul_inv, MeasureTheory.upperCrossingTime_zero', MaximalSpectrum.iInf_localization_eq_bot, Finset.Icc_bot, Algebra.IsCentral.center_eq_bot, IsGaloisGroup.fixingSubgroup_bot, Multiplicative.toAdd_bot, BddLat.coe_forget_to_semilatSup, ProperCone.mem_bot, Filter.tendsto_atBot_pure, ProbabilityTheory.indep_bot_left, GaloisConnection.l_bot, BotHom.symm_dual_id, Nat.Subtype.coe_bot, Seminorm.closedBall_bot, Submodule.lTensorOne_symm_apply, BoundedOrderHomClass.toBotHomClass, Finset.Iio_bot, IntermediateField.finInsepDegree_bot, MvPolynomial.supported_empty, ClosedSubmodule.toSubmodule_bot, LinearOrder.bot_topologicalSpace_eq_generateFrom, MeasureTheory.SimpleFunc.simpleFunc_bot, Set.Ico_bot, affineSpan_eq_bot, ProbabilityTheory.condVar_bot, fixedPoints.lfp_eq_sSup_iterate, Filter.limsup_const_bot, JacobsonNoether.exists_separable_and_not_isCentral', IsPredArchimedean.findAtom_bot, Fin.rev_last_eq_bot, Submodule.lTensorOne'_one_tmul, AlgebraicGeometry.Proj.basicOpen_zero, IntermediateField.finrank_bot', sdiff_top, Quantale.bot_mul, CategoryTheory.Pretopology.toGrothendieck_bot, Partition.bot_lt_of_mem, Setoid.mk_eq_bot, Subalgebra.rank_eq_one_iff, sdiff_bot, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingPropertyFixedBot_ι_app_bot, DiscreteTopology.eq_bot, Order.Ideal.bot_mem, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w_assoc, IntermediateField.botEquiv_def, Additive.toMul_eq_bot, Valuation.Integers.integralClosure, IntermediateField.finSepDegree_bot', HeytingHom.map_bot', stronglyMeasurable_bot_iff, ContinuousMap.concatCM_right, compl_top, IntermediateField.eq_bot_of_isSepClosed_of_isSeparable, IsSimpleOrder.lt_top_iff_eq_bot, WellFoundedLT.finite_ne_bot_of_iSupIndep, iSup_eq_if, Multiset.max_le_of_forall_le, ConditionallyCompleteLinearOrderBot.csSup_empty, FirstOrder.Language.Substructure.elementarySkolem₁Reduct.instSmall, Finset.Colex.toColex_empty, bot_bihimp, Set.Icc_bot, Subalgebra.eq_bot_of_rank_le_one, isGLB_univ, BotHom.coe_sup, IntermediateField.bot_eq_top_of_finrank_adjoin_le_one, isBot_bot, Submodule.lTensorOne_tmul, AlgebraicGeometry.IsSchemeTheoreticallyDominant.ker_eq_bot, AddCon.toSetoid_eq_bot, IntermediateField.relrank_bot_right, AlgebraicGeometry.Scheme.IdealSheafData.support_top, Subalgebra.comm_trans_lTensorBot, OrderType.bot_eq_zero, InfiniteGalois.fixedField_bot, CompletelyDistribLattice.himp_bot, IsCompl.inf_right_eq_bot_iff, NonUnitalAlgebra.map_bot, IsSepClosed.separableClosure_eq_bot_iff, Subfield.closure_empty, HeytingAlgebra.himp_bot, Order.coheight_bot_eq_krullDim, Subalgebra.bot_eq_top_of_finrank_eq_one, DiscreteQuotient.proj_bot_eq, isCompl_bot_top, AlgebraicGeometry.Scheme.basicOpen_zero, IsSimpleOrder.eq_bot_of_lt, AlgebraicGeometry.Scheme.IdealSheafData.map_bot, iInf_eq_bot, eq_bot_of_singletons_open, Subalgebra.isAlgebraic_bot_iff, disjointed_bot, TwoSidedIdeal.bot_ringCon, AlgebraicGeometry.isAffineOpen_bot, List.foldr_sup_eq_sup_toFinset, nhds_bot_order, iInf₂_eq_bot, ciSup_false, SupBotHom.coe_bot, perfectClosure.eq_bot_of_isSeparable, Order.IsSuccLimit.bot_lt, subsingleton_iff_bot_eq_top, BotHom.symm_dual_comp, ProbabilityTheory.Kernel.indep_bot_left, Finpartition.bot_notMem, Order.le_succ_bot_iff, BotHom.dual_comp, MeasureTheory.sigmaFinite_trim_bot_iff, OrdinalApprox.lfp_mem_range_lfpApprox, partialSups_bot, Partition.coe_removeBot, not_bot_lt_iff, Heyting.isRegular_bot, Ne.bot_lt', BoundedLatticeHomClass.map_bot, subsingleton_iff_top_eq_bot, BotHom.dual_id, FirstOrder.Language.Substructure.instIsEmptySubtypeMemBotOfConstants, IntermediateField.insepDegree_bot, bot_eq_zero'', IsAlgClosed.algebraicClosure_eq_bot_iff, IntermediateField.rank_bot', disjoint_iff_inf_le, IsAntichain.bot_mem_iff, Finset.sup_bot, BotHom.inf_apply, Disjoint.eq_iff, AlgebraicGeometry.genericPoint_eq_bot_of_affine, Order.lt_succ_bot_iff, Filter.blimsup_false, eq_bot_iff, MeasureTheory.condExp_bot', IsGalois.tfae, Subfield.card_bot, AlgebraicGeometry.basicOpen_eq_bot_iff, nhds_bot_basis_Iic, IntermediateField.LinearDisjoint.eq_bot_of_self, UpperSet.Ici_bot, SubRootedTree.bot_mem_iff, ProbabilityTheory.Kernel.indep_bot_right, separableClosure.separableClosure_eq_bot, SemilatSupCat_dual_comp_forget_to_partOrd, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent, NonUnitalAlgebra.mem_bot, not_isMax_bot, AlgebraicGeometry.Scheme.IdealSheafData.support_bot, Submodule.lTensorOne_one_tmul, BoxIntegral.Prepartition.notMem_bot, iSup_of_empty, CategoryTheory.sheafBotEquivalence_counitIso, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁, isLUB_empty, disjoint_self, AffineSubspace.not_wOppSide_bot, Representation.invtSubmodule.coe_bot, isLeast_bot_iff, isCompl_top_bot, Subfield.extendScalars_self, iSup_eq_bot, csInf_univ, IntermediateField.relrank_bot_left, CompleteBooleanAlgebra.inf_compl_le_bot, Subalgebra.LinearDisjoint.eq_bot_of_commute_of_self, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, Subalgebra.finrank_bot, bot_eq_zero, Module.End.invtSubmodule.mk_eq_bot_iff, ZMod.fieldRange_castHom_eq_bot, lowerBounds_univ, IsSimpleOrder.bot_lt_iff_eq_top, AlgebraicGeometry.Scheme.IdealSheafData.mul_bot, bihimp_hnot_self, Finset.fold_inf_univ, AffineSubspace.eq_bot_or_nonempty, GaloisConnection.l_u_bot, MeasureTheory.hitting_eq_sInf, Finset.sup_eq_bot_iff, IntermediateField.mem_bot, OrderIso.map_bot, Algebra.IsCentral.out, IsSimpleOrder.eq_bot_or_eq_top, GaloisCoinsertion.u_bot, SemilatSupCat.coe_forget_to_partOrd, BotHom.coe_inf, TopologicalSpace.Opens.not_nonempty_iff_eq_bot, bot_le, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom, IntermediateField.fixingSubgroup_bot, symmDiff_bot, MeasureTheory.upcrossingsBefore_bot, Subalgebra.bot_eq_top_iff_rank_eq_one, isGalois_bot, Subalgebra.rTensorBot_tmul, iSup_extend_bot, sSupHomClass.toSupBotHomClass, Set.Iio_bot, iSup_bot, isGalois_iff_isGalois_bot, Fin.rev_bot, isMin_bot, Disjoint.eq_bot, boundary_Icc, AffineSubspace.bot_parallel_iff_eq_bot, FirstOrder.Language.Substructure.fg_bot, MvPolynomial.weightedTotalDegree_zero, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁_assoc, bihimp_bot, Set.Iic.coe_bot, SetLike.isAtom_iff, min_bot_right, Set.Ici_bot, IntermediateField.finrank_adjoin_simple_eq_one_iff, CompleteLattice.ωScottContinuous.bot, boundary_product, Nat.bot_eq_zero, Subalgebra.LinearDisjoint.eq_bot_of_self, sInf_eq_bot, inf_compl_eq_bot, separableClosure.eq_bot_iff, Subalgebra.LinearDisjoint.bot_left, Subalgebra.rank_bot, eq_bot_of_minimal, Coheyting.boundary_bot, Subalgebra.LinearDisjoint.bot_right, IntermediateField.rank_adjoin_simple_eq_one_iff, Concept.extent_bot, notMem_iff_exists_ne_and_isConjRoot, Ne.bot_lt, TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete, Order.bot_lt_succ, compl_bot, AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot, Algebra.adjoin_empty, Subalgebra.fg_bot_toSubmodule, Algebra.botEquiv_symm_apply, MeasurableSpace.generateFrom_singleton_empty, NonUnitalStarAlgebra.toNonUnitalSubalgebra_bot, IccLeftChart_extend_bot_mem_frontier, BoundedOrderHom.map_bot', AffineSubspace.notMem_bot, bot_inf_eq, not_supPrime_bot, isLeast_univ, MeasureTheory.condExp_bot_ae_eq, exists_orderEmbedding_covby_of_forall_covby_finite_of_bot, Finset.Colex.ofColex_bot, Nucleus.bot_apply, DiscreteQuotient.proj_bot_injective, Seminorm.ball_bot, Subalgebra.bot_eq_top_of_rank_eq_one, RingCon.toCon_bot, Set.Intersecting.bot_notMem, CategoryTheory.Functor.WellOrderInductionData.Extension.zero_val, IsGalois.mem_bot_iff_fixed, Subalgebra.finrank_eq_one_iff, bot_notMem_iff, IntermediateField.map_bot, PrimeSpectrum.basicOpen_eq_bot_iff, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot, Finpartition.parts_inf, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact, bot_eq_one, YoungDiagram.notMem_bot, bot_eq_zero', Finpartition.avoid_parts_val, separableClosure.eq_bot_of_isPurelyInseparable, Subalgebra.eq_bot_of_isPurelyInseparable_of_isSeparable, Subalgebra.finite_bot, IntermediateField.finSepDegree_bot, Pi.isAtom_single, AddGroupTopology.toTopologicalSpace_bot, IsGaloisGroup.fixedPoints_eq_bot, IsLowerSet.bot_notMem, Finset.truncatedInf_of_notMem, SSet.skeleton_zero bridge: bot_eq_false

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_le 📖	mathematical	—	Bot.bot toBot	—	—
ext_bot 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Bot.bot toBot	—	PartialOrder.ext bot_unique bot_le
instSubsingleton 📖	mathematical	—	OrderBot Preorder.toLE PartialOrder.toPreorder	—	le_antisymm

OrderDual

Definitions

Name	Category	Theorems
instBot 📖	CompOp	20 math math: InfTopHom.symm_dual_id, TopHom.symm_dual_id, ofDual_bot, InfTopHom.symm_dual_comp, InfTopHom.dual_id, TopHom.dual_symm_apply_apply, ofAdd_bot, InfTopHom.dual_comp, WithBot.toDualTopEquiv_symm_bot, toDual_top, InfTopHom.dual_apply_toFun, TopHom.symm_dual_comp, SemilatInfCat.dual_map, WithBot.toDualTopEquiv_bot, TopHom.dual_apply_apply, InfTopHom.dual_symm_apply_toFun, toDual_eq_bot, TopHom.dual_comp, ofDual_eq_top, TopHom.dual_id
instBoundedOrder 📖	CompOp	27 math math: isCompl_toDual_iff, isCompl_ofDual_iff, BoundedLatticeHom.dual_id, BoundedOrderHom.symm_dual_id, NonemptyInterval.dual_top, BoundedLatticeHom.symm_dual_comp, BoundedOrderHom.dual_apply_toOrderHom, BddOrd.dual_map, Interval.dual_top, BoundedOrderHom.dual_id, BoundedOrderHom.symm_dual_comp, BoundedLatticeHom.dual_symm_apply_toFun, isSimpleOrder_iff_isSimpleOrder_orderDual, BddDistLat.dual_map, BoundedLatticeHom.symm_dual_id, BoundedOrderHom.dual_comp, BoolAlg.dual_map, BoundedLatticeHom.dual_apply_toFun, BoundedOrderHom.dual_symm_apply_toOrderHom, BoundedLatticeHom.dual_comp, ComplementedLattice.instOrderDual, IsCompl.dual, IncidenceAlgebra.eulerChar_orderDual, FinBddDistLat.dual_map, FinBoolAlg.dual_map, BddLat.dual_map, instIsSimpleOrder
instOrderBot 📖	CompOp	12 math math: Codisjoint.dual, SemilatInfCat.dual_obj_isOrderBot, instIsAtomic, disjoint_toDual_iff, instIsAtomistic, isAtomistic_dual_iff_isCoatomistic, codisjoint_ofDual_iff, isAtom_dual_iff_isCoatom, Finset.toDual_inf, isAtomic_dual_iff_isCoatomic, IsCoatom.dual, Finset.ofDual_sup
instOrderTop 📖	CompOp	11 math math: isCoatomic_dual_iff_isAtomic, Disjoint.dual, Finset.ofDual_inf, instIsCoatomistic, disjoint_ofDual_iff, codisjoint_toDual_iff, IsAtom.dual, isCoatomistic_dual_iff_isAtomistic, Finset.toDual_sup, instIsCoatomic, isCoatom_dual_iff_isAtom
instTop 📖	CompOp	17 math math: SupBotHom.dual_comp, SupBotHom.symm_dual_comp, BotHom.dual_apply_apply, WithTop.toDualBotEquiv_symm_top, SemilatSupCat.dual_map, SupBotHom.dual_id, BotHom.dual_symm_apply_apply, SupBotHom.symm_dual_id, toDual_eq_top, BotHom.symm_dual_id, toDual_bot, BotHom.symm_dual_comp, BotHom.dual_comp, BotHom.dual_id, WithTop.toDualBotEquiv_top, ofDual_top, ofDual_eq_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofDual_bot 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual Bot.bot instBot Top.top	—	—
ofDual_eq_bot 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual Bot.bot Top.top instTop	—	—
ofDual_eq_top 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual Top.top Bot.bot instBot	—	—
ofDual_top 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike ofDual Top.top instTop Bot.bot	—	—
toDual_bot 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual Bot.bot Top.top instTop	—	—
toDual_eq_bot 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual Bot.bot instBot Top.top	—	—
toDual_eq_top 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual Top.top instTop Bot.bot	—	—
toDual_top 📖	mathematical	—	DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike toDual Top.top Bot.bot instBot	—	—

OrderTop

Definitions

Name	Category	Theorems
toTop 📖	CompOp	1222 math, 1 bridge math: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top_iff, IsCyclotomicExtension.adjoin_primitive_root_eq_top, NonUnitalSubalgebra.center_eq_top, isMax_iff_eq_top, Nucleus.instTopHomClass, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.toPartialMap_hom, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, IntermediateField.finInsepDegree_top, HahnEmbedding.IsPartial.baseEmbedding_le, SSet.Subcomplex.preimage_eq_top_iff, IsCoatom.ne_iff_eq_top, measurable_from_top, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, ofDual_toAdd_zero, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, LinearOrderedAddCommGroupWithTop.neg_eq_top, Finset.Icc_top, IntermediateField.adjoin_eq_top_iff_of_isAlgebraic, Heyting.isRegular_top, LinearOrderedAddCommGroupWithTop.sub_pos, IsTop.eq_top, IsCompl.sup_eq_top, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, isGreatest_univ, Set.Ioc_top, TopologicalSpace.Opens.mem_top, AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, AlgebraicTopology.NormalizedMooreComplex.obj_d, MeasureTheory.Measure.sub_top, AlgebraicGeometry.Scheme.support_nilradical, BoundedOrderHomClass.map_top, FiniteArchimedeanClass.mem_addSubgroup_iff, Additive.ofMul_eq_top, InfTopHom.inf_apply, IsCofinal.singleton_top, Subalgebra.pi_top, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, Finset.truncatedSup_union_of_notMem, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, sSup_univ, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, TopHom.symm_dual_id, Multiplicative.ofAdd_eq_top, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, MeasureTheory.OuterMeasure.mkMetric_top, codisjoint_bot, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero, AffineBasis.tot, Algebra.mem_top, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, Filter.liminf_const_top, Finset.Colex.toColex_univ, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, ArchimedeanClass.closedBallAddSubgroup_top, AlgebraicGeometry.Scheme.IdealSheafData.one_eq_top, IsOpen.exists_subset_affineIndependent_span_eq_top, SSet.iSup_subcomplexOfSimplex_prod_eq_top, isSimpleOrder_iff_isAtom_top, OrdinalApprox.gfp_mem_range_gfpApprox, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, AlgebraicGeometry.Scheme.Opens.topIso_inv, CategoryTheory.Sieve.mem_iff_pullback_eq_top, Finset.inf_eq_top_iff, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, iInf_of_empty, AddValuation.top_iff, inseparable_top, BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top, TensorAlgebra.adjoin_range_ι, NonUnitalStarAlgebra.mem_top, IsCofinal.top_mem, AlgHom.equalizer_eq_top, iInf_false, AlgebraicGeometry.Scheme.Hom.id_appTop, CategoryTheory.Presheaf.imageSieve_app, iInf_eq_top, SetLike.isCoatom_iff, IsGaloisGroup.fixingSubgroup_top, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, FiniteArchimedeanClass.mk_lt_mk, Algebra.toSubsemiring_eq_top, MeasureTheory.OuterMeasure.trim_top, RootPairing.invtRootSubmodule.eq_top_iff, IsLocalRing.closedPoint_mem_iff, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, QuotientAddGroup.leftRel_eq_top, Finset.Nonempty.sup_eq_top_iff, RingCon.matrix_top, SSet.Subcomplex.range_eq_top, AlgHom.fieldRange_eq_map, Field.exists_primitive_element, isGalois_iff_isGalois_top, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, List.foldr_inf_eq_inf_toFinset, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, Coheyting.boundary_top, AlgebraicGeometry.Scheme.ι_toIso_inv, LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot, LowerSet.Iic_top, CategoryTheory.Subfunctor.range_toRange, UnitAddTorus.mFourierSubalgebra_closure_eq_top, eq_top_iff, Frm.Iso.mk_hom, BoxIntegral.Prepartition.top_boxes, Algebra.toSubring_eq_top, AddCon.toSetoid_top, LinearOrderedAddCommGroupWithTop.add_eq_top, NumberField.adjoin_eq_top_of_infinitePlace_lt, Polynomial.IsSplittingField.splits_iff, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, SSet.Subcomplex.topIso_inv_app_coe, CategoryTheory.Subobject.top_arrow_isIso, polynomialFunctions.starClosure_topologicalClosure, Coheyting.hnot_boundary, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, CategoryTheory.GrothendieckTopology.trivial_covering, hnot_symmDiff_self, AffineEquiv.span_eq_top_iff, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, AffineSubspace.direction_eq_top_iff_of_nonempty, Additive.ofMul_top, IsCompl.symmDiff_eq_top, SemilatInfCat_dual_comp_forget_to_partOrd, Set.Iio_top, add_top, induced_const, affineSpan_singleton_union_vadd_eq_top_of_span_eq_top, isMax_top, BoxIntegral.HasIntegral.tendsto, integralClosure_eq_top_iff, OrderHom.top_def, interior_convexHull_nonempty_iff_affineSpan_eq_top, CompleteSublattice.top_mem, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, TopHom.coe_top, Coheyting.hnot_eq_top_iff_exists_boundary, TopologicalSpace.eq_top_iff_forall_inseparable, MulArchimedeanClass.top_eq_mk_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.PresheafedSpace.Γ_obj_op, CategoryTheory.Subobject.map_top, IntermediateField.adjoin_univ, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, TopCat.GlueData.MkCore.V_id, AffineSubspace.linear_topEquiv, UniformSpace.toTopologicalSpace_top, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, CategoryTheory.Subfunctor.Subpresheaf.preimage_eq_top_iff, not_lt_top_iff, symmDiff_top', lt_top_of_lt, CategoryTheory.Sieve.top_apply, ContinuousMap.concatCM_left, MulAction.BlockMem.coe_top, Algebra.EssFiniteType.adjoin_mem_finset, AlgebraicGeometry.Scheme.Hom.preimage_top, Polynomial.IsSplittingField.adjoin_rootSet, AlgebraicGeometry.Scheme.isoSpec_hom, AlgebraicGeometry.Scheme.ι_toIso_inv_assoc, NonemptyInterval.dual_top, HahnEmbedding.Seed.baseEmbedding_strictMono, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, NonUnitalSubalgebra.prod_top, AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, Ne.lt_top', FiniteArchimedeanClass.val_mk, MeasurableSpace.map_const, bot_covBy_top, NonUnitalStarAlgebra.coe_top, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, Set.Icc_top, Sublocale.top_mem, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, Subalgebra.center_eq_top, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, FiniteArchimedeanClass.mem_ballAddSubgroup_iff, SSet.iSup_skeleton, PrimeSpectrum.iSup_basicOpen_eq_top_iff, IsNormalClosure.adjoin_rootSet, AffineBasis.tot', himp_top, TopologicalSpace.Opens.isOpenEmbedding_obj_top, AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, Fin.top_eq_last, UpperSet.Ioi_top, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, TopHom.coe_inf, SSet.Subcomplex.eq_top_iff_of_hasDimensionLT, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, BoxIntegral.IntegrationParams.eventually_isPartition, iInf₂_eq_top, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc, disjoint_top, essInf_measure_zero, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, Polynomial.SplittingFieldAux.adjoin_rootSet, RingCon.subsingleton_quotient, CategoryTheory.Sieve.generate_top, SSet.Subcomplex.topIso_inv_ι, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top, IntermediateField.fixingSubgroup_top, AffineSubspace.coe_eq_univ_iff, CategoryTheory.Sieve.equalizer_self, TopologicalSpace.Opens.mk_univ, top_bihimp, CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, inf_top_eq, LatticeHom.withTopWithBot'_toFun, Codisjoint.top_le, Finset.Ici_eq_Icc, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, IsCoatom.sup_eq_top_of_ne, PMF.toOuterMeasure_caratheodory, not_top_lt, BoxIntegral.Prepartition.isPartitionTop, Filter.Eventually.lt_top_iff_ne_top, Fin.rev_top, IntermediateField.relfinrank_top_right, Order.succ_top, IndiscreteTopology.eq_top, Finset.Icc_bot_top, liminf_eq_top, FiniteMulArchimedeanClass.withTopOrderIso_apply_coe, Set.Ioi_top, AlgebraicGeometry.Scheme.Hom.toPartialMap_domain, CompleteLinearOrder.top_sdiff, HahnEmbedding.Partial.isWF_support_evalCoeff, Submodule.toConvexCone_top, HahnEmbedding.Partial.orderTop_eq_iff, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, ArchimedeanClass.top_eq_mk_iff, AlgebraicGeometry.Scheme.Γ_obj, CategoryTheory.Presieve.isSheafFor_top_sieve, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Scheme.IdealSheafData.instIsEmptyCarrierCarrierCommRingCatSubschemeTop, SSet.hasDimensionLT_subcomplex_top_iff, IntermediateField.restrictScalars_top, nhds_top_basis_Ici, Fintype.IsSimpleOrder.univ, EuclideanGeometry.Sphere.orthRadius_center, Representation.invtSubmodule.coe_top, Finset.top_eq_univ, TopologicalSpace.isOpen_top_iff, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.preimage_basicOpen_top, Fin.top_eq_zero, MvPolynomial.adjoin_range_X, sup_top_eq, AlgebraicGeometry.Scheme.ΓSpecIso_inv, NonUnitalAlgebra.range_id, IntermediateField.mem_top, AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, Field.primitive_element_iff_algHom_eq_of_eval', codisjoint_iff, CategoryTheory.GrothendieckTopology.top_mem, TopHom.dual_symm_apply_apply, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', Flag.top_mem, adjoin_eq_top_of_conductor_eq_top, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top, IntermediateField.relrank_top_right, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, Finset.truncatedSup_empty, Algebra.coe_top, TopologicalSpace.Opens.inclusion'_top_functor, MeasureTheory.Measure.mkMetric_top, Set.instNonemptyTop, Set.Ici_top, SSet.Subcomplex.eq_top_iff_contains_nonDegenerate, max_top_right, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, Subalgebra.unop_top, BoxIntegral.Prepartition.compl_top, ProperCone.innerDual_zero, Finpartition.top_isEquipartition, AlgebraicGeometry.PresheafedSpace.Γ_map_op, Order.Ideal.IsProper.top_notMem, ofAdd_bot, Order.pred_top_le_iff, BoxIntegral.Prepartition.biUnion_top, Finpartition.parts_top_subset, AlgebraicGeometry.Scheme.id_appTop, sSup_compact_eq_top, LinearOrderedAddCommGroupWithTop.sub_top, isGLB_empty, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, Codisjoint.eq_top_of_le, BoundedLatticeHom.coe_comp_lattice_hom', Convex.interior_nonempty_iff_affineSpan_eq_top, Polynomial.adjoin_rootSet_eq_range, CategoryTheory.Presheaf.equalizerSieve_self_eq_top, CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, HahnEmbedding.IsPartial.strictMono, Multiset.inf_zero, ClosedSubmodule.bot_orthogonal_eq_top, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, TopCat.Presheaf.map_germ_eq_Γgerm, Algebra.top_toSubmodule, SSet.Subcomplex.preimage_range, AlgebraicGeometry.Scheme.ker_of_isAffine, Subalgebra.fg_of_submodule_fg, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, Filter.tendsto_atTop_pure, map_eq_top_iff, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, FiniteMulArchimedeanClass.mem_ballSubgroup_iff, CliffordAlgebra.adjoin_range_ι, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, Codisjoint.eq_top_of_self, Polynomial.Splits.adjoin_rootSet_eq_range, ArchimedeanClass.ballAddSubgroup_top, Setoid.top_def, codisjoint_self, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, IntermediateField.lift_top, min_top_left, iSup_eq_top, Interval.dual_top, FiniteArchimedeanClass.liftOrderHom_mk, TopHom.sup_apply, List.min_le_of_le, AlgebraicGeometry.ΓSpec.adjunction_counit_app, isCoatomic_iff, AlgebraicGeometry.tilde.isoTop_hom, CategoryTheory.Subfunctor.range_eq_top, borel_eq_top_of_discrete, FiniteMulArchimedeanClass.mem_closedBallSubgroup_iff, ClosedSubmodule.top_orthogonal_eq_bot, le_top, CoheytingHomClass.map_top, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum, CategoryTheory.Subfunctor.Subpresheaf.image_top, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous, AlgebraicGeometry.Γ_restrict_isLocalization, IntermediateField.restrictScalars_eq_top_iff, Set.Icc_bot_top, not_infPrime_top, HahnEmbedding.IsPartial.truncLT_mem_range, IsUpperSet.top_mem, Complementeds.coe_top, CategoryTheory.top_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, AlgebraicGeometry.ΓSpecIso_obj_hom, LinearOrderedAddCommGroupWithTop.neg_pos, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁, sup_hnot_self, Set.Ioc.coe_top, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one, Setoid.mk_eq_top, MeasureTheory.OuterMeasure.comap_top, CategoryTheory.Sieve.overEquiv_top, ProbabilityTheory.iIndep_comap_mem_iff, Field.exists_primitive_element_of_finite_bot, CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem, TopologicalSpace.Opens.functor_obj_map_obj, CategoryTheory.Sieve.arrows_eq_top_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, Finset.Iic_top, CategoryTheory.Sieve.arrows_top, Frm.Iso.mk_inv, QuotientAddGroup.rightRel_eq_top, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, IsCoatom.Ici_eq, AffineSubspace.mem_top, Algebra.bijective_algebraMap_iff, Subalgebra.topEquiv_apply, CategoryTheory.topologyOfClosureOperator_sieves, hnot_top, Field.exists_primitive_element_of_finite_top, CategoryTheory.Subobject.isIso_top_arrow, IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic, continuous_top, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, essInf_const_top, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, LinearOrderedAddCommGroupWithTop.top_pos, himp_eq_top_iff, ArchimedeanClass.mk_zero, LatticeHom.withTop'_toFun, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AddGroupTopology.toTopologicalSpace_top, top_inf_eq, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, IntermediateField.rank_top, CompleteDistribLattice.top_sdiff, CategoryTheory.Sieve.generate_of_singleton_isSplitEpi, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, CategoryTheory.Sieve.functorPullback_top, max_eq_top, Finset.truncatedSup_singleton, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, WithTop.pred_eq_top, NonUnitalAlgebra.top_toNonUnitalSubsemiring, Quotient.subsingleton_iff, IsUpperSet.top_notMem, PowerBasis.adjoin_gen_eq_top, BoundedLatticeHom.map_top', StarSubalgebra.eq_top_iff, Finset.Colex.ofColex_top, UpperSet.Ioi_eq_top, IntermediateField.adjoin_root_eq_top, codisjoint_iff_le_sup, FiniteMulArchimedeanClass.withTopOrderIso_symm_apply, FiniteArchimedeanClass.mem_closedBallAddSubgroup_iff, AffineSubspace.smul_top, ConvexCone.toPointedCone_top, OrderIsoClass.toTopHomClass, Order.pred_lt_top, iInf_ne_top_subtype, CategoryTheory.GrothendieckTopology.discrete_eq_top, TopCat.Presheaf.map_germ_eq_Γgerm_assoc, FiniteArchimedeanClass.mem_ball_iff, NonUnitalStarAlgebra.top_toNonUnitalSubalgebra, Set.addCentralizer_empty, CoheytingHom.map_top', Finset.Ioi_eq_Ioc, MeasureTheory.OuterMeasure.zero_caratheodory, Finset.fold_sup_univ, ConvexCone.mem_top, IsLprojection.coe_top, LinearOrderedAddCommGroupWithTop.add_lt_top, FiniteMulArchimedeanClass.liftOrderHom_mk, IsMax.eq_top, MeasureTheory.OuterMeasure.top_caratheodory, Multiset.inf_coe, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, IntermediateField.finrank_top, Finset.sup_eq_top_iff, hnot_bot, WithTop.subtypeOrderIso_symm_apply, Multiplicative.toAdd_eq_top, NonUnitalStarAlgebra.range_eq_top, separableClosure.eq_top_iff, ProbabilityTheory.iIndepSet.iIndep_comap_mem, Algebra.top_toSubring, AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty, AlgebraicGeometry.ΓSpec.left_triangle, CategoryTheory.Subfunctor.eq_top_iff_isIso, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, AlgebraicGeometry.AffineSpace.comp_homOfVector, IntermediateField.top_toSubalgebra, IntermediateField.relrank_top_left, AddValuation.map_zero, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, AlgebraicGeometry.Scheme.homOfLE_appTop, SemilatInfCat.coe_forget_to_partOrd, GaloisConnection.u_eq_top, IsGaloisGroup.fixedPoints_bot, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, nhds_top, AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom, HahnEmbedding.Partial.eval_smul, IsCoatomic.eq_top_or_exists_le_coatom, exists_root_adjoin_eq_top_of_isCyclic, grade_top, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', upperBounds_univ, isLUB_univ, FiniteArchimedeanClass.subsemigroup_eq_addSubgroup, AlgebraicGeometry.Scheme.isoSpec_Spec_hom, Filter.Eventually.ne_top_of_lt, sSup_atoms_eq_top, NonemptyInterval.coe_top_interval, IntermediateField.finrank_eq_one_iff_eq_top, SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, TopHom.inf_apply, AlgebraicGeometry.tilde.isIso_toOpen_top, SupHom.withTop'_toFun, codisjoint_top_left, lt_top_iff_ne_top, Subfield.extendScalars_top, AlgebraicGeometry.HasRingHomProperty.appTop, AffineSubspace.mk'_top, Algebra.zariskisMainProperty_iff_exists_saturation_eq_top, NumberField.is_primitive_element_of_infinitePlace_lt, StrictAnti.apply_eq_top_iff, CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top, MonoidAlgebra.exists_finset_adjoin_eq_top, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, IntermediateField.bot_eq_top_of_rank_adjoin_eq_one, SeparationQuotient.inseparableSetoid_eq_top_iff, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.Scheme.IdealSheafData.mul_top, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, Filter.OrderTop.atTop_eq, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd, CategoryTheory.ObjectProperty.IsStrongGenerator.subobject_eq_top, PowerBasis.adjoin_eq_top_of_gen_mem_adjoin, NonUnitalAlgebra.eq_top_iff, AlgebraicGeometry.SheafedSpace.Γ_map, Polynomial.IsSplittingField.adjoin_rootSet', AlgebraicGeometry.germ_stalkClosedPointIso_hom, bddLat_dual_comp_forget_to_semilatSupCat, ProbabilityTheory.Kernel.iIndep_comap_mem_iff, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, BoxIntegral.Prepartition.iUnion_top, BoxIntegral.Prepartition.distortion_top, ProperCone.dual_zero, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, OrdinalApprox.gfpApprox_ord_eq_gfp, CategoryTheory.Coverage.eq_top_pullback, BoundedOrderHom.coe_comp_topHom, AlgebraicGeometry.Scheme.toIso_inv_ι_assoc, AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, AlgebraicGeometry.Scheme.toSpecΓ_appTop, Order.Ideal.top_toLowerSet, Order.Coframe.top_sdiff, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff, CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top', Order.krullDim_le_one_iff_of_boundedOrder, AlgHom.range_eq_top, CategoryTheory.Subfunctor.Subpresheaf.epi_iff_range_eq_top, NonUnitalAlgebra.mem_top, Set.top_eq_univ, NonUnitalStarAlgebra.toNonUnitalSubalgebra_eq_top, SSet.Subcomplex.image_top, isLUB_atoms_top, Set.Ici.coe_top, LinearOrderedAddCommGroupWithTop.neg_top, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty, MulArchimedeanClass.mk_one, Interval.coe_top, IsCoatom.lt_iff, AffineSubspace.topEquiv_symm_apply_coe, FrameHom.coe_toInfTopHom, AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective, Module.End.invtSubmodule.mk_eq_top_iff, TopologicalSpace.Opens.inclusion'_map_eq_top, InfHom.withTop'_toFun, Subalgebra.centralizer_eq_top_iff_subset, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty, Set.Iic_top, MeasureTheory.Measure.add_top, Heyting.Regular.coe_top, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, Algebra.top_toSubsemiring, AlgebraicGeometry.Scheme.IdealSheafData.map_top, IsLocalRing.PrimeSpectrum.asIdeal_top, PseudoEpimorphismClass.toTopHomClass, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, WithTop.orderPred_top, AlgebraicGeometry.Scheme.Opens.ι_appTop, IsCoatom.covBy_top, AffineMap.map_top_of_surjective, AlgebraicGeometry.Scheme.map_basicOpen, bddLat_dual_comp_forget_to_semilatInfCat, CategoryTheory.Subfunctor.Subpresheaf.top_obj, NonUnitalAlgebra.adjoin_univ, AlgebraicGeometry.isRetrocompact_basicOpen, Tropical.le_zero, Order.pred_top_lt_iff, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, IntermediateField.bot_eq_top_iff_finrank_eq_one, FrameHom.map_sSup', AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff, ArchimedeanClass.out_top, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, CategoryTheory.Sieve.pullback_eq_top_of_mem, AlgebraicGeometry.Scheme.comp_appTop_assoc, AlgebraicGeometry.Proj.basicOpen_one, GaloisConnection.u_top, FiniteMulArchimedeanClass.mk_le_mk, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, Order.coheight_top, nhds_top_order, CompletelyDistribLattice.top_sdiff, isGreatest_top_iff, RestrictedProduct.isEmbedding_inclusion_top, Subalgebra.op_top, AlgebraicGeometry.Scheme.isoSpec_Spec, ArchimedeanClass.ball_top, CategoryTheory.Subfunctor.Subpresheaf.range_id, Order.isPredPrelimit_top, Order.PFilter.top_mem, FiniteArchimedeanClass.mk_le_mk, Field.exists_primitive_element_iff_finite_intermediateField, CategoryTheory.ExtremalEpi.subobject_eq_top, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, Field.Emb.Cardinal.filtration_apply, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, BoxIntegral.Prepartition.splitMany_empty, indiscreteTopology_iff, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, Subalgebra.bot_eq_top_iff_finrank_eq_one, Order.height_top_eq_krullDim, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, AddMonoidAlgebra.exists_finset_adjoin_eq_top, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, CategoryTheory.Subfunctor.instIsIsoFunctorTypeιTop, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, Ordinal.enum_succ_eq_top, IsLowerSet.top_mem, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.SheafedSpace.Γ_obj_op, Algebra.isAlgebraic_iff, TopologicalSpace.Closeds.coe_top, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, NonUnitalStarAlgebra.comap_top, CategoryTheory.Dial.tensorUnit_rel, bot_codisjoint, FreeAlgebra.adjoin_range_ι, ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, max_top_left, WithTop.pred_top, min_top_right, ClosedSubmodule.orthogonal_eq_top_iff, FiniteMulArchimedeanClass.mem_subgroup_iff, SSet.Subcomplex.topIso_inv_ι_assoc, AlgebraicGeometry.Scheme.inv_appTop, IntermediateField.finrank_top', AlgebraicGeometry.isLocalization_away_of_isAffine, CategoryTheory.SemilatticeInf.tensorUnit, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AffineSubspace.direction_top, Affine.Simplex.span_eq_top, IsSimpleOrder.equivBool_symm_apply, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, IccRightChart_extend_top_mem_frontier, WithBot.sInf_empty, TopologicalSpace.Opens.eq_bot_or_top, AlgebraicGeometry.morphismRestrict_appTop, isSimpleOrder_iff, IsLocalRing.closed_point_mem_iff, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, Algebra.IsAlgebraic.isNormalClosure_iff, iInf_top, AlgebraicGeometry.Scheme.Hom.preimage_opensRange, StarSubalgebra.toSubalgebra_eq_top, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, List.le_min_of_forall_le, StarSubalgebra.mem_top, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, CategoryTheory.GrothendieckTopology.bot_covering, AlgebraicGeometry.LocallyRingedSpace.Γ_map, Finset.max_eq_top, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, covBy_top_iff, exists_subset_affineIndependent_affineSpan_eq_top, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, FiniteMulArchimedeanClass.congrOrderIso_symm, SemilatInfCat.Iso.mk_inv_toFun, Additive.toMul_top, bot_lt_top, Algebra.adjoin_adjoin_coe_preimage, AlgebraicGeometry.eq_top_of_sigmaSpec_subset_of_isCompact, Algebra.adjoin_top, FrameHomClass.toInfTopHomClass, bihimp_self, HahnEmbedding.ArchimedeanStrata.isInternal_stratum', AlgebraicGeometry.PresheafedSpace.Γ_obj, IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top, AffineSubspace.perpBisector_eq_top, MeasureTheory.condExpIndL1Fin_disjoint_union, Algebra.adjoin_root_eq_top_of_isSplittingField, not_isMin_top, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, Algebra.surjective_algebraMap_iff, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, TopHom.coe_sup, IsCoatom.le_iff, Field.primitive_element_iff_minpoly_degree_eq, FiniteMulArchimedeanClass.min_le_mk_mul, Algebra.toSubmodule_eq_top, AlgHom.fieldRange_eq_top, Ne.lt_top, Finset.inf_empty, DualNumber.range_inlAlgHom_sup_adjoin_eps, AlgebraicGeometry.Scheme.toOpen_eq, isPurelyInseparable_iff_perfectClosure_eq_top, Fin.cast_top, top_disjoint, BoundedLatticeHomClass.map_top, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, bot_himp, inf_eq_top_iff, Algebra.adjoin_univ, AlgHom.equalizer_same, CategoryTheory.Subobject.mk_eq_top_of_isIso, CategoryTheory.Subfunctor.image_top, PUnit.top_eq, TopologicalSpace.Closeds.coe_eq_univ, hahnEmbedding_isOrderedModule_rat, FiniteArchimedeanClass.congrOrderIso_symm, AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one, IntermediateField.adjoin_root_eq_top_of_isSplittingField, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, TopHom.top_apply, algebraicClosure.eq_top_iff, AddAction.BlockMem.coe_top, IsOpen.exists_between_affineIndependent_span_eq_top, Setoid.eq_top_iff, AffineSubspace.top_coe, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, ClosureOperator.closure_top, Field.primitive_element_iff_minpoly_natDegree_eq, sInfHom.coe_top, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, Subalgebra.fg_top, le_top, NonUnitalAlgebra.toSubmodule_eq_top, CategoryTheory.Subobject.top_eq_id, AlgebraicGeometry.Scheme.Hom.inv_appTop, SSet.iSup_skeletonOfMono, affineSpan_coe_preimage_eq_top, AffineSubspace.pointwise_vadd_top, Complementeds.mk_top, TwoSidedIdeal.top_ringCon, AffineSubspace.perpBisector_self, codisjoint_top_right, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, GaloisConnection.u_l_top, AlgebraicGeometry.Spec_zeroLocus, ProperCone.innerDual_empty, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, IntermediateField.topEquiv_symm_apply_coe, top_sup_eq, affineSpan_eq_top_of_nonempty_interior, OrderIso.map_top, TopHom.symm_dual_comp, FiniteArchimedeanClass.withTopOrderIso_symm_apply, CategoryTheory.Limits.equalizerSubobject_of_self, SSet.iSup_range_eq_top_of_isColimit, IntermediateField.rank_top', Subalgebra.topEquiv_symm_apply_coe, HahnEmbedding.Partial.mem_domain, AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app, MeasureTheory.OuterMeasure.boundedBy_top, AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective, iInf_eq_dif, ofDual_toAdd_eq_top_iff, CompleteSublattice.coe_top, IntermediateField.topEquiv_apply, MulArchimedeanClass.out_top, HahnEmbedding.Seed.mem_domain_baseEmbedding, CategoryTheory.Subobject.top_factors, AlgebraicGeometry.basicOpen_eq_of_affine', LowerAdjoint.closure_top, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AffineSubspace.topEquiv_apply, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem, iInf_extend_top, IsCyclotomicExtension.singleton_one, MeasureTheory.hittingBtwn_eq_sInf, InfTopHom.coe_top, SSet.finite_subcomplex_top_iff, CategoryTheory.Subobject.eq_top_of_isIso_arrow, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, Algebra.adjoin_restrictScalars, top_add, NonUnitalAlgebra.coe_top, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range, QuotientGroup.rightRel_eq_top, NonUnitalAlgebra.map_top, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.Scheme.topIso_hom, SemilatInfCat.dual_map, MeasurableSpace.generateFrom_singleton, AlgebraicGeometry.finite_appTop_of_universallyClosed, AffineSubspace.span_univ, IntermediateField.top_toSubfield, TopologicalSpace.IsOpenCover.iSup_eq_top, LinearOrderedAddCommMonoidWithTop.top_add', NonUnitalAlgebra.to_subring_eq_top, eq_top_of_bot_isCompl, RingOfIntegers.exponent_eq_one_iff, Codisjoint.out, sSup_eq_top, BoxIntegral.integrable_iff_cauchy, AlgebraicGeometry.specTargetImageFactorization_app_injective, MulArchimedeanClass.ballSubgroup_top, Algebra.comap_top, Finset.inf_erase_top, CategoryTheory.Subobject.underlyingIso_inv_top_arrow_assoc, AlgebraicGeometry.PresheafedSpace.Γ_map, NonUnitalAlgebra.toNonUnitalSubring_eq_top, top_le_iff, FiniteArchimedeanClass.addSubgroup_strictAnti, AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective, CategoryTheory.Subobject.isIso_arrow_iff_eq_top, Codisjoint.eq_iff, ClosedSubmodule.mem_top, TopHom.dual_apply_apply, CategoryTheory.Sieve.functorInclusion_top_isIso, CompleteBooleanAlgebra.top_le_sup_compl, AffineBasis.isUnit_toMatrix_iff, FiniteMulArchimedeanClass.ballSubgroup_strictAnti, Set.exists_seq_iSup_eq_top_iff_countable, Fin.rev_zero_eq_top, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, Order.not_isPredLimit_top, sInfHomClass.toInfTopHomClass, AffineSubspace.instNonemptySubtypeMemTop, AlgebraicGeometry.affineAnd_apply, Concept.intent_top, IntermediateField.fg_top, isTop_iff_eq_top, instDiscreteMeasurableSpace, MeasureTheory.OuterMeasure.top_apply', AlgebraicGeometry.AffineSpace.reindex_appTop_coord, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, List.foldr_min_of_ne_nil, IsCyclotomicExtension.iff_adjoin_eq_top, CategoryTheory.Subobject.underlyingIso_inv_top_arrow, SemilatInfCat.Iso.mk_hom_toFun, AlgEquiv.fieldRange_eq_top, Field.Emb.Cardinal.iSup_adjoin_eq_top, AlgebraicGeometry.ΓSpec.toSpecΓ_of, FiniteArchimedeanClass.coe_congrOrderIso_apply, DiscreteQuotient.instSubsingletonQuotientTop, symmDiff_hnot_self, Finset.Ioi_top, sInf_diff_singleton_top, top_mem_upperBounds, tendsto_atTop_nhds, Set.centralizer_empty, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, CategoryTheory.Subobject.underlyingIso_top_hom, StrictMono.apply_eq_top_iff, AlgebraicGeometry.IsAffine.affine, StarSubalgebra.coe_top, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, AlgebraicGeometry.SheafedSpace.Γ_obj, ProperCone.dual_empty, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top, ArchimedeanClass.mk_eq_top_iff, AlgebraicGeometry.Scheme.mem_basicOpen_top, sdiff_top, ConvexCone.isGenerating_top, AlgebraicTopology.NormalizedMooreComplex.objX_zero, Set.Iic.coe_top, WellFoundedGT.induction_top, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, FiniteMulArchimedeanClass.subgroup_eq_bot, Algebra.eq_top_iff, Filter.liminf_bot, AffineSubspace.comap_top, fourierSubalgebra_closure_eq_top, top_notMem_iff, himp_self, Filter.limsInf_bot, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, NonUnitalStarAlgebra.range_id, Subalgebra.prod_top, CategoryTheory.Sieve.overEquiv_symm_top, MulArchimedeanClass.closedBallSubgroup_top, NonUnitalAlgebra.comap_top, MeasureTheory.Measure.toOuterMeasure_top, hnot_sup_self, NonUnitalStarAlgebra.map_top, AlgebraicGeometry.Scheme.comp_appTop, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, subalgebra_top_finrank_eq_submodule_top_finrank, IntermediateField.adjoin_eq_top_iff, Fin.range_natAdd_eq_Ioi, BoxIntegral.Prepartition.split_of_notMem_Ioo, IsCyclotomicExtension.Rat.adjoin_singleton_eq_top, AlgebraicGeometry.Scheme.fromSpecStalk_app, MulArchimedeanClass.mk_eq_top_iff, WithTop.subtypeOrderIso_apply_coe, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, CategoryTheory.Subobject.pullback_top, AlgebraicGeometry.isField_of_universallyClosed, polynomialFunctions.topologicalClosure, sInf_empty, RingCon.range_mkₐ, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst, ContinuousMap.concatCM_right, FiniteArchimedeanClass.ballAddSubgroup_strictAnti, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, compl_top, IsSimpleOrder.lt_top_iff_eq_bot, MeasurableSpace.map_top, CategoryTheory.Subobject.epi_iff_mk_eq_top, RootPairing.coe_top, Algebra.map_top, Concept.extent_top, CategoryTheory.Subfunctor.top_obj, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top, FiniteArchimedeanClass.submodule_strictAnti, CategoryTheory.Sieve.functorPushforward_top, NonUnitalStarSubalgebra.center_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_top, IntermediateField.bot_eq_top_of_finrank_adjoin_le_one, CategoryTheory.Presieve.isSeparatedFor_top, BoundedOrderHomClass.toTopHomClass, AlgebraicGeometry.Scheme.IdealSheafData.support_top, CategoryTheory.Subobject.isIso_iff_mk_eq_top, AlgebraicGeometry.Scheme.map_basicOpen_map, ClosedSubmodule.coe_top, CompleteLattice.ωScottContinuous.top, CategoryTheory.Subobject.pullback_self, BoundedLatticeHom.coe_toInfTopHom, StarAlgHom.range_eq_map_top, AlgebraicGeometry.Scheme.Hom.comp_appTop, NonUnitalStarAlgebra.eq_top_iff, Subalgebra.bot_eq_top_of_finrank_eq_one, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AddValuation.mem_supp_iff, RingCon.toCon_eq_top, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, MeasureTheory.OuterMeasure.map_top_of_surjective, isAtom_iff_eq_top, Finpartition.parts_top_subsingleton, FiniteMulArchimedeanClass.subsemigroup_eq_subgroup, isCompl_bot_top, AlgebraicGeometry.Scheme.IdealSheafData.top_mul, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, MvPolynomial.supported_univ, conductor_eq_top_iff_adjoin_eq_top, Codisjoint.eq_top_of_ge, fixedPoints.gfp_eq_sInf_iterate, BddLat.coe_forget_to_semilatInf, IsMaxChain.top_mem, isAtom_top, ArchimedeanClass.eq_zero_or_top_of_archimedean, AdjoinRoot.adjoinRoot_eq_top, AlgebraicGeometry.Scheme.IsLocallyDirected.V_self, Nucleus.coe_top, borel_eq_top_of_countable, CategoryTheory.GrothendieckTopology.top_mem', TopCat.Presheaf.Γgerm_res_apply, IntermediateField.extendScalars_top, subsingleton_iff_bot_eq_top, ConvexCone.coe_top, MeasurableSpace.measurableSet_top, CategoryTheory.Presheaf.equalizerSieve_eq_top_iff, IntermediateField.fixedField_bot, NonUnitalAlgebra.range_eq_top, IsCoatom.lt_top, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, FiniteMulArchimedeanClass.val_mk, FiniteArchimedeanClass.ball_strictAnti, FrameHom.toFun_eq_coe, ArchimedeanClass.orderHom_top, AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc, top_himp, LT.lt.lt_top, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, Complex.adjoin_I, HahnEmbedding.Partial.eval_zero, SSet.Subcomplex.range_eq_top_iff, Con.toSetoid_top, AlgebraicGeometry.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, ContinuousMap.elemental_id_eq_top, HahnSeries.finiteArchimedeanClassOrderIso_apply, MeasureTheory.OuterMeasure.map_top, Algebra.FiniteType.out, subsingleton_iff_top_eq_bot, polynomialFunctions_closure_eq_top', AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial, Projectivization.Subspace.span_univ, AlgebraicGeometry.Scheme.toIso_inv_ι, WithTop.coe_top_lt, IsSimpleOrder.eq_top_of_lt, FiniteArchimedeanClass.min_le_mk_add, TopHom.dual_comp, ClosedSubmodule.toSubmodule_top, OpenSubgroup.toOpens_top, eq_top_of_isCompl_bot, iInf_eq_if, TopologicalSpace.Opens.map_top, CategoryTheory.Functor.imageSieve_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, CategoryTheory.Sieve.pullback_top, Set.not_top_subset, IntermediateField.insepDegree_top, FiniteMulArchimedeanClass.mk_lt_mk, ProjectiveSpectrum.basicOpen_one, BoundedLatticeHom.coe_comp_inf_hom', AlgebraicGeometry.Scheme.Γevaluation_naturality, RingCon.coe_top, OpenAddSubgroup.toOpens_top, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, CategoryTheory.Sieve.uliftFunctorInclusion_top_isIso, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, nhds_top_basis, NonUnitalStarSubalgebra.prod_top, ext_top, Finset.inf_top, LinearOrderedAddCommGroupWithTop.top_add', Sum.Lex.inr_top, AlgebraicGeometry.Spec.fromSpecStalk_eq, NonUnitalAlgebra.top_toSubring, ContinuousMapZero.elemental_eq_top, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, SemilatSupCat_dual_comp_forget_to_partOrd, IntermediateField.fg_top_iff, CategoryTheory.GrothendieckTopology.top_covers, CategoryTheory.Presieve.factorsThru_top, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', induced_top, AlgebraicGeometry.Scheme.IdealSheafData.support_bot, AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq, IntermediateField.relfinrank_top_left, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, BoundedLatticeHom.coe_comp_inf_hom, sInf_eq_top, iInf_neg, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, Finset.truncatedSup_infs_of_notMem, GroupTopology.toTopologicalSpace_top, Fin.val_top, iInf_lt_top, Con.toSetoid_eq_top, MeasureTheory.OuterMeasure.dirac_caratheodory, IntermediateField.finSepDegree_top, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject_top, SSet.N.iSup_subcomplex_eq_top, Nucleus.top_apply, IsOpen.affineSpan_eq_top, CategoryTheory.Sieve.id_mem_iff_eq_top, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, IsAdjoinRoot.primitive_element_root, Set.Icc.coe_top, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, Order.IsPredLimit.lt_top, AlgebraicGeometry.Scheme.Opens.ι_image_top, BoundedLatticeHomClass.toInfTopHomClass, isCompl_top_bot, Field.Emb.Cardinal.adjoin_basis_eq_top, NonUnitalAlgebra.top_toSubmodule, Algebra.TensorProduct.adjoin_tmul_eq_top, AlgebraicGeometry.Scheme.Γ_obj_op, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints, BiheytingAlgebra.top_sdiff, SSet.Subcomplex.topIso_hom, CategoryTheory.Sieve.pullback_ofObjects_eq_top, HahnEmbedding.Partial.exists_domain_eq_top, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, FiniteMulArchimedeanClass.subgroup_strictAnti, AlgebraicGeometry.Scheme.IdealSheafData.radical_top, AlgebraicGeometry.Scheme.Opens.topIso_hom, MeasureTheory.OuterMeasure.top_apply, Order.Ideal.coe_top, CategoryTheory.presheafIsGeneratedBy_of_isFinite, IsSimpleOrder.bot_lt_iff_eq_top, Subalgebra.restrictScalars_top, QuotientGroup.leftRel_eq_top, PrimeSpectrum.basicOpen_one, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, MeasureTheory.Measure.top_add, AlgebraicGeometry.AffineSpace.map_appTop_coord, top_symmDiff', AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, isCofinal_iff_top_mem, PrimeSpectrum.iSup_basicOpen_eq_top_iff', Filter.bliminf_false, MeasureTheory.hitting_eq_sInf, AlgebraicGeometry.isIso_fromTildeΓ_iff, top_sdiff', InfTopHom.coe_inf, AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv, polynomialFunctions_closure_eq_top, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, IsSimpleOrder.eq_bot_or_eq_top, IsDedekindDomain.integer_univ, InfTopHom.top_apply, bihimp_top, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, LT.lt.eq_top, AlgebraicGeometry.Scheme.IdealSheafData.comap_top, IsAdjoinRoot.adjoin_root_eq_top, NonUnitalAlgebra.toNonUnitalSubring_top, iInf_emptyset, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, CategoryTheory.PreOneHypercover.sieve₀_trivial, CategoryTheory.Subfunctor.preimage_eq_top_iff, CategoryTheory.Subfunctor.Subpresheaf.eq_top_iff_isIso, iSup₂_eq_top, CategoryTheory.Dial.tensorUnitImpl_rel, ofAdd_toDual_eq_zero_iff, Finset.Ioc_top, CategoryTheory.Presieve.isSheafFor_top, Order.succ_le_iff_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, Subalgebra.bot_eq_top_iff_rank_eq_one, IntermediateField.coe_top, FiniteArchimedeanClass.addSubgroup_eq_bot, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, min_eq_top, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, HahnEmbedding.Partial.exists_isMax, Fin.zero_eq_top, eq_top_or_lt_top, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, IccRightChart_extend_top, Algebra.range_id, Polynomial.SplittingField.adjoin_rootSet, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, isSplittingField_iff_intermediateField, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, Finset.truncatedSup_of_notMem, Fin.rev_bot, ClosureOperator.isClosed_top, NonemptyInterval.coe_top, boundary_Icc, TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr, Polynomial.adjoin_X, bihimp_eq_top, TopologicalSpace.Opens.coe_top, CategoryTheory.Subfunctor.epi_iff_range_eq_top, CategoryTheory.PreOneHypercover.sieve₁_trivial, StarSubalgebra.top_toSubalgebra, BoxIntegral.Prepartition.mem_top, BoundedOrderHom.map_top', IsSimpleOrder.equivBool_apply, CategoryTheory.Subfunctor.Subpresheaf.range_eq_top, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, boundary_product, instIndiscreteTopology, OrderIsoClass.toInfTopHomClass, NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top, TopologicalSpace.Opens.coe_eq_univ, HahnEmbedding.Seed.domain_baseEmbedding, Field.primitive_element_iff_algHom_eq_of_eval, Set.setOf_top, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, Additive.toMul_eq_top, FiniteArchimedeanClass.withTopOrderIso_apply_coe, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, CategoryTheory.Subfunctor.range_id, FiniteMulArchimedeanClass.coe_congrOrderIso_apply, separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable, AddCon.toSetoid_eq_top, Set.Iic.eq_top_iff, AlgebraicGeometry.instIsAffineHomιBasicOpen, Codisjoint.eq_top, compl_bot, Finset.Ici_top, not_infIrred_top, Icc_isBoundaryPoint_top, FiniteArchimedeanClass.mem_closedBall_iff, CategoryTheory.Sieve.generate_of_contains_isSplitEpi, Subalgebra.rank_top, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, Subalgebra.bot_eq_top_of_rank_eq_one, MulArchimedeanClass.orderHom_top, sInfHom.top_apply, ArchimedeanClass.closedBall_top, CategoryTheory.Subfunctor.Subpresheaf.range_toRange, AlgebraicGeometry.SheafedSpace.restrictTopIso_hom, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, MeasureTheory.OuterMeasure.toMeasure_top, hahnEmbedding_isOrderedAddMonoid, Prop.top_eq_true, Multiplicative.toAdd_top, subalgebra_top_rank_eq_submodule_top_rank, isComplemented_top, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot, AlgebraicGeometry.SheafedSpace.Γ_map_op, TopHom.dual_id, RingCon.toCon_top, Multiplicative.ofAdd_top, isCyclic_tfae, isTop_top, affineSpan_eq_top_iff_nonempty_of_subsingleton, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, GaloisInsertion.l_top, CategoryTheory.GrothendieckTopology.top_covering, Filter.limsSup_top, hahnEmbedding_isOrderedModule, Fin.succ_top, AlgebraicGeometry.LocallyRingedSpace.Γ_obj, CoheytingAlgebra.top_sdiff, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, IntermediateField.sepDegree_top, IsAntichain.top_mem_iff, Order.Ideal.principal_top, CategoryTheory.Limits.kernelSubobject_zero, AlgebraicGeometry.Scheme.toSpecΓ_base, HahnEmbedding.Partial.toOrderAddMonoidHom_injective bridge: top_eq_true

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_top 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Top.top toTop	—	PartialOrder.ext top_unique le_top
instSubsingleton 📖	mathematical	—	OrderTop Preorder.toLE PartialOrder.toPreorder	—	ge_antisymm
le_top 📖	mathematical	—	Top.top toTop	—	—

Pi

Definitions

Name	Category	Theorems
instBotForall 📖	CompOp	39 math math: CategoryTheory.isCoseparating_empty_of_thin, CategoryTheory.isCodetecting_empty_of_groupoid, LinearGrowth.linearGrowthInf_bot, SupHom.coe_bot, Polynomial.roots_eq_zero_iff_isRoot_eq_bot, CategoryTheory.ObjectProperty.isCodetecting_bot_of_isGroupoid, LinearGrowth.linearGrowthSup_bot, sSupHom.coe_bot, SimpleGraph.singletonSubgraph_adj, CategoryTheory.ObjectProperty.isDetecting_bot_of_isGroupoid, Pairwise.disjoint_extend_bot, limsup_eq_bot, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, Directed.extend_bot, Irreducible.isRoot_eq_bot_of_natDegree_ne_one, Sym2.fromRel_bot_iff, bot_comp, bot_apply, CategoryTheory.isSeparating_empty_of_thin, BotHom.coe_bot, Set.pairwise_bot_iff, Ideal.Filtration.bot_N, MeasureTheory.upperCrossingTime_zero, isAtom_iff_eq_single, Filter.coprodᵢ_eq_bot_iff, Filter.coprodᵢ_bot', Sym2.fromRel_bot, CategoryTheory.ObjectProperty.isSeparating_bot_of_isThin, bot_def, Filter.coprodᵢ_eq_bot_iff', eq_bot_iff, Polynomial.roots_eq_zero_iff_eq_zero_or_isRoot_eq_bot, SupBotHom.coe_bot, CategoryTheory.isDetecting_empty_of_groupoid, InfHom.coe_bot, CategoryTheory.ObjectProperty.isCoseparating_bot_of_isThin, iSup_extend_bot, CompleteLattice.ωScottContinuous.bot, isAtom_single
instBoundedOrder 📖	CompOp	1 math math: isCompl_iff
instOrderBot 📖	CompOp	12 math math: ContinuousAt.finset_sup, Continuous.finset_sup, Filter.Tendsto.finset_sup_nhds, ContinuousWithinAt.finset_sup, isAtom_iff_eq_single, isAtom_iff, ContinuousOn.finset_sup, isAtomistic, Finset.sup_apply, disjoint_iff, isAtomic, isAtom_single
instOrderTop 📖	CompOp	9 math math: isCoatomistic, ContinuousAt.finset_inf, ContinuousOn.finset_inf, Finset.inf_apply, ContinuousWithinAt.finset_inf, codisjoint_iff, isCoatomic, Continuous.finset_inf, Filter.Tendsto.finset_inf_nhds
instTopForall 📖	CompOp	48 math math: LinearGrowth.linearGrowthSup_top, CategoryTheory.ObjectProperty.topEquivalence_counitIso, TopHom.coe_top, Sym2.fromRel_top, CategoryTheory.Functor.isLeftAdjoint_iff_rightAdjointObjIsDefined_eq_top, SimpleGraph.preconnected_iff_reachable_eq_top, liminf_eq_top, LinearGrowth.linearGrowthInf_top, CategoryTheory.ObjectProperty.topEquivalence_unitIso, Setoid.top_def, Ideal.Filtration.top_N, Matrix.toBlock_mul_eq_mul, SupHom.coe_top, Setoid.mk_eq_top, CategoryTheory.ObjectProperty.instIsSerreClassTop, CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsTop, top_def, CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallyLarge_top, CategoryTheory.ObjectProperty.instContainsZeroTopOfHasZeroObject, Quot.subsingleton_iff, CategoryTheory.exists_equivalence_iff_of_locallySmall, CategoryTheory.ObjectProperty.instEssentiallySmallTopOfEssentiallySmall, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, top_apply, CategoryTheory.ObjectProperty.ι_map_top, CategoryTheory.ObjectProperty.IsLocal.top, CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsTop, sInfHom.coe_top, MeasureTheory.OuterMeasure.boundedBy_top, iInf_extend_top, InfTopHom.coe_top, top_comp, CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsTop, CategoryTheory.IsCardinalFilteredGenerator.of_isDense, ExpGrowth.expGrowthSup_top, CategoryTheory.Functor.isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top, CompleteLattice.ωScottContinuous.top, ExpGrowth.expGrowthInf_top, Nucleus.coe_top, RingCon.coe_top, MeasureTheory.extend_top, PresheafOfModules.pullbackObjIsDefined_eq_top, CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsTop, Set.pairwise_top, CategoryTheory.ObjectProperty.topEquivalence_inverse, CategoryTheory.ObjectProperty.topEquivalence_functor, Sym2.fromRel_top_iff, InfHom.coe_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_apply 📖	mathematical	—	Bot.bot instBotForall	—	—
bot_comp 📖	mathematical	—	Bot.bot instBotForall	—	—
bot_def 📖	mathematical	—	Bot.bot instBotForall	—	—
top_apply 📖	mathematical	—	Top.top instTopForall	—	—
top_comp 📖	mathematical	—	Top.top instTopForall	—	—
top_def 📖	mathematical	—	Top.top instTopForall	—	—

Prod

Definitions

Name	Category	Theorems
instBot 📖	CompOp	2 math math: snd_bot, fst_bot
instBoundedOrder 📖	CompOp	2 math math: IncidenceAlgebra.eulerChar_prod, isCompl_iff
instOrderBot 📖	CompOp	2 math math: Finset.sup_prodMap, disjoint_iff
instOrderTop 📖	CompOp	2 math math: Finset.inf_prodMap, codisjoint_iff
instTop 📖	CompOp	2 math math: snd_top, fst_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst_bot 📖	mathematical	—	Bot.bot instBot	—	—
fst_top 📖	mathematical	—	Top.top instTop	—	—
snd_bot 📖	mathematical	—	Bot.bot instBot	—	—
snd_top 📖	mathematical	—	Top.top instTop	—	—

Subtype

Definitions

Name	Category	Theorems
boundedOrder 📖	CompOp	2 math math: BoundedLatticeHom.subtypeVal_coe, BoundedLatticeHom.subtypeVal_apply
orderBot 📖	CompOp	3 math math: Finset.sup_coe, SupBotHom.subtypeVal_coe, SupBotHom.subtypeVal_apply
orderTop 📖	CompOp	3 math math: InfTopHom.subtypeVal_coe, Finset.inf_coe, InfTopHom.subtypeVal_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_bot 📖	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder	—	—	mk_bot
coe_eq_bot_iff 📖	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder	—	—	coe_bot
coe_eq_top_iff 📖	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder	—	—	coe_top
coe_top 📖	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder	—	—	mk_top
mk_bot 📖	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder	—	—	le_bot_iff coe_le_coe bot_le
mk_eq_bot_iff 📖	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder	—	—	coe_eq_bot_iff
mk_eq_top_iff 📖	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder	—	—	coe_eq_top_iff
mk_top 📖	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder	—	—	top_le_iff coe_le_coe le_top

ULift

Definitions

Name	Category	Theorems
instBot 📖	CompOp	2 math math: down_bot, up_bot
instBoundedOrder 📖	CompOp	—
instOrderBot 📖	CompOp	—
instOrderTop 📖	CompOp	—
instTop 📖	CompOp	2 math math: down_top, up_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
down_bot 📖	mathematical	—	Bot.bot instBot	—	—
down_top 📖	mathematical	—	Top.top instTop	—	—
up_bot 📖	mathematical	—	Bot.bot instBot	—	—
up_top 📖	mathematical	—	Top.top instTop	—	—

(root)

Definitions

Name	Category	Theorems
BoundedOrder 📖	CompData	1 math math: BoundedOrder.instSubsingleton
OrderBot 📖	CompData	1 math math: OrderBot.instSubsingleton
OrderTop 📖	CompData	1 math math: OrderTop.instSubsingleton
botOrderOrNoBotOrder 📖	CompOp	—
topOrderOrNoTopOrder 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_eq_false 📖	bridging (complete)	—	Bot.bot OrderBot.toBot BoundedOrder.toOrderBot Bool.instBoundedOrder	Bot.bot	—
bot_le 📖	mathematical	—	Bot.bot OrderBot.toBot	—	OrderBot.bot_le
bot_lt_iff_ne_bot 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Bot.bot OrderBot.toBot Preorder.toLE	—	LE.le.lt_iff_ne' bot_le
bot_lt_of_lt 📖	mathematical	Preorder.toLT	Bot.bot OrderBot.toBot Preorder.toLE	—	lt_of_lt_of_le' bot_le
bot_lt_top 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Bot.bot OrderBot.toBot Preorder.toLE BoundedOrder.toOrderBot Top.top OrderTop.toTop BoundedOrder.toOrderTop	—	lt_top_iff_ne_top bot_ne_top
bot_ne_top 📖	—	—	—	—	not_subsingleton subsingleton_of_bot_eq_top
bot_notMem_iff 📖	mathematical	—	Set Set.instMembership Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	Ne.bot_lt LT.lt.false
bot_unique 📖	—	Preorder.toLE PartialOrder.toPreorder Bot.bot OrderBot.toBot	—	—	LE.le.antisymm' bot_le
dite_ne_bot 📖	—	—	—	—	—
dite_ne_top 📖	—	—	—	—	—
eq_bot_iff 📖	mathematical	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder	—	le_bot_iff
eq_bot_mono 📖	—	Preorder.toLE PartialOrder.toPreorder Bot.bot OrderBot.toBot	—	—	bot_unique
eq_bot_of_bot_eq_top 📖	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderBot Top.top OrderTop.toTop BoundedOrder.toOrderTop	—	—	eq_bot_mono le_top
eq_bot_of_minimal 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Bot.bot OrderBot.toBot Preorder.toLE	—	eq_bot_or_bot_lt
eq_bot_of_top_eq_bot 📖	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderTop Bot.bot OrderBot.toBot BoundedOrder.toOrderBot	—	—	eq_bot_mono le_top
eq_bot_or_bot_lt 📖	mathematical	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	LE.le.eq_or_lt' bot_le
eq_top_iff 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder	—	top_le_iff
eq_top_mono 📖	—	Preorder.toLE PartialOrder.toPreorder Top.top OrderTop.toTop	—	—	top_unique
eq_top_of_bot_eq_top 📖	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderBot Top.top OrderTop.toTop BoundedOrder.toOrderTop	—	—	eq_top_mono bot_le
eq_top_of_top_eq_bot 📖	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderTop Bot.bot OrderBot.toBot BoundedOrder.toOrderBot	—	—	eq_top_mono bot_le
eq_top_or_lt_top 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	LE.le.eq_or_lt le_top
isBot_bot 📖	mathematical	—	IsBot Bot.bot OrderBot.toBot	—	bot_le
isBot_iff_eq_bot 📖	mathematical	—	IsBot Preorder.toLE PartialOrder.toPreorder Bot.bot OrderBot.toBot	—	IsMin.eq_of_ge IsBot.isMin bot_le
isMax_iff_eq_top 📖	mathematical	—	IsMax Preorder.toLE PartialOrder.toPreorder Top.top OrderTop.toTop	—	IsMax.eq_of_le le_top
isMax_top 📖	mathematical	—	IsMax Preorder.toLE Top.top OrderTop.toTop	—	IsTop.isMax isTop_top
isMin_bot 📖	mathematical	—	IsMin Preorder.toLE Bot.bot OrderBot.toBot	—	IsBot.isMin isBot_bot
isMin_iff_eq_bot 📖	mathematical	—	IsMin Preorder.toLE PartialOrder.toPreorder Bot.bot OrderBot.toBot	—	IsMin.eq_of_ge bot_le
isTop_iff_eq_top 📖	mathematical	—	IsTop Preorder.toLE PartialOrder.toPreorder Top.top OrderTop.toTop	—	IsMax.eq_of_le IsTop.isMax le_top
isTop_top 📖	mathematical	—	IsTop Top.top OrderTop.toTop	—	le_top
ite_ne_bot 📖	—	—	—	—	dite_ne_bot
ite_ne_top 📖	—	—	—	—	dite_ne_top
le_bot_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Bot.bot OrderBot.toBot	—	LE.le.ge_iff_eq' bot_le
le_top 📖	mathematical	—	Top.top OrderTop.toTop	—	OrderTop.le_top
lt_top_iff_ne_top 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Top.top OrderTop.toTop Preorder.toLE	—	LE.le.lt_iff_ne le_top
lt_top_of_lt 📖	mathematical	Preorder.toLT	Top.top OrderTop.toTop Preorder.toLE	—	lt_of_lt_of_le le_top
ne_bot_of_gt 📖	—	Preorder.toLT	—	—	LT.lt.ne' LT.lt.trans_le' bot_le
ne_bot_of_le_ne_bot 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	LT.lt.ne' LE.le.trans_lt' Ne.bot_lt
ne_top_of_le_ne_top 📖	—	Preorder.toLE PartialOrder.toPreorder	—	—	LT.lt.ne LE.le.trans_lt Ne.lt_top
ne_top_of_lt 📖	—	Preorder.toLT	—	—	LT.lt.ne LT.lt.trans_le le_top
not_bot_lt_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Bot.bot OrderBot.toBot Preorder.toLE	—	Iff.not_left bot_lt_iff_ne_bot
not_isBot_iff_ne_bot 📖	mathematical	—	IsBot Preorder.toLE PartialOrder.toPreorder	—	Iff.not isBot_iff_eq_bot
not_isMax_bot 📖	mathematical	—	IsMax Preorder.toLE PartialOrder.toPreorder Bot.bot OrderBot.toBot	—	exists_ne le_bot_iff bot_le
not_isMax_iff_ne_top 📖	mathematical	—	IsMax Preorder.toLE PartialOrder.toPreorder	—	Iff.not isMax_iff_eq_top
not_isMin_iff_ne_bot 📖	mathematical	—	IsMin Preorder.toLE PartialOrder.toPreorder	—	Iff.not isMin_iff_eq_bot
not_isMin_top 📖	mathematical	—	IsMin Preorder.toLE PartialOrder.toPreorder Top.top OrderTop.toTop	—	exists_ne top_le_iff le_top
not_isTop_iff_ne_top 📖	mathematical	—	IsTop Preorder.toLE PartialOrder.toPreorder	—	Iff.not isTop_iff_eq_top
not_lt_bot 📖	mathematical	—	Preorder.toLT Bot.bot OrderBot.toBot Preorder.toLE	—	IsMin.not_lt isMin_bot
not_lt_top_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Top.top OrderTop.toTop Preorder.toLE	—	Iff.not_left lt_top_iff_ne_top
not_top_lt 📖	mathematical	—	Preorder.toLT Top.top OrderTop.toTop Preorder.toLE	—	IsMax.not_lt isMax_top
subsingleton_iff_bot_eq_top 📖	mathematical	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderBot Top.top OrderTop.toTop BoundedOrder.toOrderTop	—	subsingleton_of_bot_eq_top
subsingleton_iff_top_eq_bot 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderTop Bot.bot OrderBot.toBot BoundedOrder.toOrderBot	—	subsingleton_of_top_eq_bot
subsingleton_of_bot_eq_top 📖	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderBot Top.top OrderTop.toTop BoundedOrder.toOrderTop	—	—	subsingleton_of_top_le_bot ge_of_eq
subsingleton_of_top_eq_bot 📖	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder BoundedOrder.toOrderTop Bot.bot OrderBot.toBot BoundedOrder.toOrderBot	—	—	subsingleton_of_top_le_bot le_of_eq
subsingleton_of_top_le_bot 📖	—	Preorder.toLE PartialOrder.toPreorder Top.top OrderTop.toTop BoundedOrder.toOrderTop Bot.bot OrderBot.toBot BoundedOrder.toOrderBot	—	—	le_antisymm le_trans le_top bot_le
top_eq_true 📖	bridging (complete)	—	Top.top OrderTop.toTop BoundedOrder.toOrderTop Bool.instBoundedOrder	Top.top	—
top_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Top.top OrderTop.toTop	—	LE.le.ge_iff_eq le_top
top_ne_bot 📖	—	—	—	—	not_subsingleton subsingleton_of_top_eq_bot
top_notMem_iff 📖	mathematical	—	Set Set.instMembership Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder Preorder.toLT	—	Ne.lt_top LT.lt.false
top_unique 📖	—	Preorder.toLE PartialOrder.toPreorder Top.top OrderTop.toTop	—	—	LE.le.antisymm le_top

---

← Back to Index