| Metric | Count |
|---|
DefinitionsorderTop, orderBot, instDecidableIsLeast, tacticBddDefault | 4 |
Theoremsdual, exists_ge, insert, inter_of_left, inter_of_right, mono, union, dual, exists_le, insert, inter_of_left, inter_of_right, mono, union, isCofinalFor_fst_image_prod_snd_image, le_of_maximal, le_of_minimal, maximal_iff_isGreatest, minimal_iff_isLeast, isCofinalFor, isCoinitialFor, iscofinalfor, iscoinitialfor, mono_left, mono_right, of_subset, rfl, trans, mono_left, mono_right, of_subset, rfl, trans, bddBelow, dual, exists_between, exists_between', insert, inter_Iic_of_mem, lowerBounds_eq, mono, nonempty, of_subset_of_superset, prod, union, unique, bddAbove, dual, insert, isGreatest_iff_eq, isLUB, lt_iff, mono, nonempty, union, unique, upperBounds_eq, bddAbove, dual, exists_between, exists_between', insert, inter_Ici_of_mem, mono, nonempty, of_subset_of_superset, prod, union, unique, upperBounds_eq, bddBelow, dual, insert, isGLB, isLeast_iff_eq, lowerBounds_eq, lt_iff, mono, nonempty, union, unique, lowerBounds_univ, upperBounds_univ, bddBelow, lowerBounds_univ, bddAbove, upperBounds_univ, bddAbove_lowerBounds, bddBelow_upperBounds, subsingleton_of_isLUB_le_isGLB, bddAbove_Icc, bddAbove_Ico, bddAbove_Iic, bddAbove_Iio, bddAbove_Ioc, bddAbove_Ioo, bddAbove_def, bddAbove_empty, bddAbove_iff_exists_ge, bddAbove_iff_subset_Iic, bddAbove_insert, bddAbove_preimage_ofDual, bddAbove_preimage_toDual, bddAbove_singleton, bddAbove_union, bddBelow_Icc, bddBelow_Ici, bddBelow_Ico, bddBelow_Ioc, bddBelow_Ioi, bddBelow_Ioo, bddBelow_bddAbove_iff_subset_Icc, bddBelow_def, bddBelow_empty, bddBelow_iff_exists_le, bddBelow_iff_subset_Ici, bddBelow_insert, bddBelow_preimage_ofDual, bddBelow_preimage_toDual, bddBelow_singleton, bddBelow_union, bot_mem_lowerBounds, exists_glb_Ioi, exists_lub_Iio, glb_Ioi_eq_self_or_Ioi_eq_Ici, isGLB_Icc, isGLB_Ici, isGLB_Ico, isGLB_Ioc, isGLB_Ioi, isGLB_Ioo, isGLB_congr, isGLB_empty, isGLB_empty_iff, isGLB_iff_le_iff, isGLB_le_isLUB, isGLB_lt_iff, isGLB_lt_isLUB_of_ne, isGLB_pair, isGLB_singleton, isGLB_univ, isGLB_upperBounds, isGreatest_Icc, isGreatest_Iic, isGreatest_Ioc, isGreatest_compl, isGreatest_himp, isGreatest_pair, isGreatest_singleton, isGreatest_top_iff, isGreatest_union_iff, isGreatest_univ, isGreatest_univ_iff, isLUB_Icc, isLUB_Ico, isLUB_Iic, isLUB_Iio, isLUB_Ioc, isLUB_Ioo, isLUB_congr, isLUB_empty, isLUB_empty_iff, isLUB_iff_le_iff, isLUB_le_iff, isLUB_lowerBounds, isLUB_lt_iff, isLUB_pair, isLUB_singleton, isLUB_univ, isLeast_Icc, isLeast_Ici, isLeast_Ico, isLeast_bot_iff, isLeast_hnot, isLeast_pair, isLeast_sdiff, isLeast_singleton, isLeast_union_iff, isLeast_univ, isLeast_univ_iff, le_glb_Ioi, le_isGLB_iff, le_of_isGLB_Ioi, le_of_isLUB_Iio, le_of_isLUB_le_isGLB, lowerBounds_Icc, lowerBounds_Ici, lowerBounds_Ico, lowerBounds_Ioc, lowerBounds_Ioi, lowerBounds_Ioo, lowerBounds_empty, lowerBounds_insert, lowerBounds_le_upperBounds, lowerBounds_mono, lowerBounds_mono_mem, lowerBounds_mono_of_isCoinitialFor, lowerBounds_mono_set, lowerBounds_prod, lowerBounds_singleton, lowerBounds_union, lt_isGLB_iff, lt_isLUB_iff, lub_Iio_eq_self_or_Iio_eq_Iic, lub_Iio_le, maximal_iff_isGreatest, mem_lowerBounds, mem_lowerBounds_iff_subset_Ici, mem_upperBounds, mem_upperBounds_iff_subset_Iic, minimal_iff_isLeast, nonempty_of_not_bddAbove, nonempty_of_not_bddBelow, not_bddAbove_iff, not_bddAbove_iff', not_bddAbove_univ, not_bddBelow_iff, not_bddBelow_iff', not_bddBelow_univ, subset_lowerBounds_upperBounds, subset_upperBounds_lowerBounds, top_mem_upperBounds, union_lowerBounds_subset_lowerBounds_inter, union_upperBounds_subset_upperBounds_inter, upperBounds_Icc, upperBounds_Ico, upperBounds_Iic, upperBounds_Iio, upperBounds_Ioc, upperBounds_Ioo, upperBounds_empty, upperBounds_insert, upperBounds_mono, upperBounds_mono_mem, upperBounds_mono_of_isCofinalFor, upperBounds_mono_set, upperBounds_prod, upperBounds_singleton, upperBounds_union | 239 |
| Total | 243 |