| Metric | Count |
|---|
DefinitionsClosedIciTopology, ClosedIicTopology, OrderClosedTopology | 3 |
Theoremsclosure, of_closure, closure, of_closure, isClosed_Ici, isClosed_Iic, if_le, max, min, eventually_lt, closure_le, nhdsGE, nhdsGT, nhdsLE, nhdsLT, Iio_eq_biUnion, Ioi_eq_biUnion, exists_between, exists_ge, exists_ge', exists_gt, exists_le, exists_le', exists_lt, orderDual, of_predOrder_succOrder, eventually_const_le, eventually_const_lt, eventually_le_const, eventually_lt, eventually_lt_const, max, max_left, max_right, min, min_left, min_right, tendsto_nhds_max_left, tendsto_nhds_max_right, tendsto_nhds_min_left, tendsto_nhds_min_right, Icc_mem_nhds, Icc_mem_nhdsGE, Icc_mem_nhdsGE_of_mem, Icc_mem_nhdsGT, Icc_mem_nhdsGT_of_mem, Icc_mem_nhdsLE, Icc_mem_nhdsLE_of_mem, Icc_mem_nhdsLT, Icc_mem_nhdsLT_of_mem, Ici_mem_nhds, Ico_mem_nhds, Ico_mem_nhdsGE, Ico_mem_nhdsGE_of_mem, Ico_mem_nhdsGT, Ico_mem_nhdsGT_of_mem, Ico_mem_nhdsLE_of_mem, Ico_mem_nhdsLT, Ico_mem_nhdsLT_of_mem, Iic_mem_nhds, Iio_mem_nhds, Ioc_mem_nhds, Ioc_mem_nhdsGE_of_mem, Ioc_mem_nhdsGT, Ioc_mem_nhdsGT_of_mem, Ioc_mem_nhdsLE, Ioc_mem_nhdsLE_of_mem, Ioc_mem_nhdsLT, Ioc_mem_nhdsLT_of_mem, Ioi_mem_nhds, Ioo_mem_nhds, Ioo_mem_nhdsGE_of_mem, Ioo_mem_nhdsGT, Ioo_mem_nhdsGT_of_mem, Ioo_mem_nhdsLE_of_mem, Ioo_mem_nhdsLT, Ioo_mem_nhdsLT_of_mem, Ioo_subset_closure_interior, epigraph, hypograph, isClosed_le, range_of_tendsto, range_of_tendsto, isClosed_le', to_t2Space, orderClosedTopology', nhdsGE_eq_nhds, nhdsGT_eq_nhdsNE, nhdsLE, nhdsLT, instOrderClosedTopology, nhdsGE, nhdsGT, nhdsLE_eq_nhds, nhdsLT_eq_nhdsNE, bddAbove_closure, bddBelow_closure, closure_Icc, closure_Ici, closure_Iic, closure_le_eq, closure_lt_subset_le, continuousWithinAt_Icc_iff_Ici, continuousWithinAt_Icc_iff_Iic, continuousWithinAt_Ico_iff_Ici, continuousWithinAt_Ico_iff_Iio, continuousWithinAt_Ioc_iff_Iic, continuousWithinAt_Ioc_iff_Ioi, continuousWithinAt_Ioo_iff_Iio, continuousWithinAt_Ioo_iff_Ioi, continuous_if_le, continuous_max, continuous_min, disjoint_nhds_atBot, disjoint_nhds_atBot_iff, disjoint_nhds_atTop, disjoint_nhds_atTop_iff, eventually_ge_nhds, eventually_gt_nhds, eventually_le_nhds, eventually_lt_nhds, frontier_Ici_subset, frontier_Iic_subset, frontier_le_subset_eq, frontier_lt_subset_eq, ge_of_tendsto, ge_of_tendsto', ge_of_tendsto_of_frequently, iInf_eq_of_forall_le_of_tendsto, iSup_eq_of_forall_le_of_tendsto, iUnion_Ici_eq_Ioi_of_lt_of_tendsto, iUnion_Iic_eq_Iio_of_lt_of_tendsto, inf_nhds_atBot, inf_nhds_atTop, instClosedIciTopology, instClosedIciTopologyOrderDual, instClosedIicTopology, instClosedIicTopologyOrderDual, instFirstCountableTopologyOrderDual, instOrderClosedTopologyForall, instOrderClosedTopologyOrderDual, instOrderClosedTopologyProd, instSecondCountableTopologyOrderDual, instSeparableSpaceOrderDual, interior_Iio, interior_Ioi, interior_Ioo, isClosed_Icc, isClosed_Ici, isClosed_Iic, isClosed_antitone, isClosed_antitoneOn, isClosed_le, isClosed_le_prod, isClosed_monotone, isClosed_monotoneOn, isOpen_Iio, isOpen_Ioi, isOpen_Ioo, isOpen_lt, isOpen_lt_prod, le_of_tendsto, le_of_tendsto', le_of_tendsto_of_frequently, le_of_tendsto_of_tendsto, le_of_tendsto_of_tendsto', le_of_tendsto_of_tendsto_of_frequently, le_on_closure, lowerBounds_closure, lt_subset_interior_le, nhdsWithin_Icc_eq_nhdsGE, nhdsWithin_Icc_eq_nhdsLE, nhdsWithin_Ico_eq_nhdsGE, nhdsWithin_Ico_eq_nhdsLT, nhdsWithin_Ioc_eq_nhdsGT, nhdsWithin_Ioc_eq_nhdsLE, nhdsWithin_Ioo_eq_nhdsGT, nhdsWithin_Ioo_eq_nhdsLT, not_tendsto_atBot_of_tendsto_nhds, not_tendsto_atTop_of_tendsto_nhds, not_tendsto_nhds_of_tendsto_atBot, not_tendsto_nhds_of_tendsto_atTop, tendsto_le_of_eventuallyLE, upperBounds_closure | 184 |
| Total | 187 |