| Name | Category | Theorems |
|---|
instBooleanAlgebra 📖 | CompOp | 211 mathmath: pairwiseDisjoint_range_iff, pairwise_disjoint_Ioc_zpow, pairwise_disjoint_Ioo_add_zsmul, inter_symmDiff_distrib_left, functorToTypes_obj, Finite.inf_of_right, CategoryTheory.Limits.Types.binaryCofan_isColimit_iff, Sym2.disjoint_diagSet_fromRel, disjoint_compl_left_iff_subset, pairwise_disjoint_Ico_zsmul, SSet.degenerate_eq_top_of_hasDimensionLT, pairwise_disjoint_Ioo_mul_zpow, AntitoneOn.set_prod, MeasureTheory.preimage_spanningSetsIndex_singleton, sdiff_singleton_wcovBy, image_symmDiff, Finset.disjoint_coe, Finset.pairwiseDisjoint_coe, disjoint_of_subset_iff_left_eq_empty, BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff, SetRel.core_mono, toFinset_symmDiff, isCompl_range_some_none, biUnion_range_succ_disjointed, indicator_symmDiff, pairwise_disjoint_fiber, Disjoint.of_image, PartialEquiv.disjointUnion_eq_piecewise, symmDiff_def, covBy_iff_exists_sdiff_singleton, instWellFoundedLTSubtypeSetFinite, SetRel.prod_comp_prod, disjoint_image_left, sdiff_singleton_covBy, MeasureTheory.spanningSetsIndex_eq_iff, Types.monoOverEquivalenceSet_inverse_map, SSet.Subcomplex.degenerate_eq_top_iff, pairwise_disjoint_Ioc_zsmul, disjointed_eq_inter_compl, subset_compl_iff_disjoint_right, mem_symmDiff, SetRel.image_core_gc, disjoint_sdiff_inter, pairwise_disjoint_Ioo_add_intCast, covBy_insert, HasSubset.Subset.disjoint_compl_right, Monotone.set_prod, iUnion_disjointed, disjoint_of_sSup_disjoint, Codisjoint.preimage, SSet.nonDegenerate_eq_bot_of_hasDimensionLT, Disjoint.set_prod_left, SimpleGraph.edgeSet_eq_iff, pairwise_disjoint_Ioc_add_zsmul, disjoint_powerset_insert, disjoint_toFinset, pairwise_disjoint_Ioc_mul_zpow, pairwise_disjoint_Ico_mul_zpow, offDiag_mono, Sylow.orbit_eq_top, SimpleGraph.disjoint_edgeSet, SSet.hasDimensionLT_iff, MeasurableSet.coe_bot, union_symmDiff_subset, SSet.skeleton_obj_eq_top, Monotone.relComp, pairwise_disjoint_Ico_add_intCast, subset_diff, Int.isCompl_even_odd, Antitone.set_prod, MonoidWithZeroHom.ValueGroup₀.restrict₀_range_eq_top, CategoryTheory.Subfunctor.Subpresheaf.bot_obj, Finite.toFinset_symmDiff, nsmul_right_monotone, mulIndicator_symmDiff, disjoint_prod, Subgroup.closure_mul_image_mul_eq_top, indicator_eq_zero', disjoint_image_iff, disjoint_pi, MvPolynomial.zeroLocus_bot, indicator_eq_zero, empty_covBy_singleton, disjoint_of_sSup_disjoint_of_le_of_le, ContinuousMap.sublattice_closure_eq_top, fintypeToFinBoolAlgOp_map, pow_right_monotone, typeToBoolAlgOp_map, apply_indicator_symmDiff, disjoint_compl_right_iff_subset, pairwise_disjoint_Ioo_zpow, Finite.inf_of_left, gc_Ici_sInf, subset_symmDiff_union_symmDiff_right, disjoint_image_image, symmDiff_subset_union, Function.disjoint_mulSupport_iff, SimpleGraph.compl_neighborSet_disjoint, biUnion_Iic_disjointed, CategoryTheory.Subfunctor.Subpresheaf.top_obj, zero_mem_neg_add_iff, pairwise_disjoint_Ioc_intCast, subset_compl_iff_disjoint_left, Types.monoOverEquivalenceSet_functor_map, pairwise_disjoint_Ioo_zsmul, CategoryTheory.Limits.Types.isPushout_of_bicartSq, Pi.support_single_disjoint, HasSubset.Subset.disjoint_compl_left, SimpleGraph.fromEdgeSet_disjoint, MeasureTheory.NullMeasurableSet.disjointed, SetRel.image_mono, Function.Injective.image_strictMono, CategoryTheory.Subfunctor.bot_obj, locallyFinsuppWithin.logCounting_divisor, disjoint_image_right, Types.monoOverEquivalenceSet_functor_obj, MeasureTheory.mem_disjointed_spanningSetsIndex, Function.mulSupport_disjoint_iff, pairwise_disjoint_Ioc_add_intCast, eq_top_of_card_le_of_finite, Finite.symmDiff_congr, inter_symmDiff_distrib_right, SetRel.preimage_mono, Finset.coe_symmDiff, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, mulIndicator_eq_one', Function.support_disjoint_iff, isCompl_range_inl_range_inr, MeasureTheory.OuterMeasure.isCaratheodory_disjointed, one_notMem_inv_mul_iff, Disjoint.set_prod_right, preimage_eq_empty_iff, SSet.horn_obj_zero, disjoint_image_inl_image_inr, disjoint_sdiff_left, gc_sSup_Iic, pairwise_disjoint_Ico_zpow, SSet.skeletonOfMono_obj_eq_top, disjoint_preimage_iff, apply_mulIndicator_symmDiff, SimpleGraph.IsCompleteBetween.disjoint, disjoint_sdiff_right, zero_notMem_sub_iff, one_notMem_div_iff, Finite.disjoint_toFinset, MeasurableSet.disjointed, pairwiseDisjoint_range_singleton, SSet.HasDimensionLT.degenerate_eq_top, MeasurableSet.coe_top, Finite.symmDiff, disjoint_diagonal_offDiag, SetRel.gc_leftDual_rightDual, symmDiff_eq_empty, mulIndicator_eq_one, Types.monoOverEquivalenceSet_inverse_obj, one_mem_div_iff, disjointed_subset, pairwise_disjoint_Ico_intCast, MvPolynomial.zeroLocus_top, SimpleGraph.disjoint_fromEdgeSet, CategoryTheory.Subfunctor.top_obj, Disjoint.of_preimage, pairwiseDisjoint_fiber, Disjoint.image, zero_notMem_neg_add_iff, disjoint_image_inl_range_inr, subsingleton_setOf_mem_iff_pairwise_disjoint, pairwiseDisjoint_image_right_iff, Types.monoOverEquivalenceSet_unitIso, MonotoneOn.set_prod, symmDiff_nonempty, preimage_symmDiff, IsCompl.preimage, functorToTypes_map, Finite.sup, Nat.isCompl_even_odd, subset_image_symmDiff, zero_mem_sub_iff, preimage_find_eq_disjointed, pairwiseDisjoint_image_left_iff, monotone_image, wcovBy_insert, instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty, covBy_iff_exists_insert, disjoint_range_inl_image_inr, pairwise_disjoint_Ico_add_zsmul, CompactSpace.elim_nhds_subcover, PairwiseDisjoint.prod, pairwiseDisjoint_pi, Types.monoOverEquivalenceSet_counitIso, MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq, fintypeToFinBoolAlgOp_obj, Disjoint.preimage, PMF.support_uniformOfFintype, Pi.mulSupport_mulSingle_disjoint, prod_subset_compl_diagonal_iff_disjoint, Disjoint.set_pi, irreducibleSpace_def, MeasureTheory.sum_restrict_disjointed_spanningSets, symmDiff_union_subset, pairwise_disjoint_Ioo_intCast, biUnion_Ioc_disjointed_of_monotone, MeasureTheory.IsSetRing.disjointed_mem, Function.disjoint_support_iff, union_symmDiff_union_subset, one_mem_inv_mul_iff, subset_symmDiff_union_symmDiff_left, disjoint_univ_pi, typeToBoolAlgOp_obj, pairwiseDisjoint_singleton_iff_injOn, disjoint_image_of_injective
|
instHImp 📖 | CompOp | 9 mathmath: IsClopen.himp, Topology.IsConstructible.himp, MeasurableSet.bihimp, MeasurableSet.himp, Definable.himp, MeasurableSet.coe_himp, TopologicalSpace.Clopens.coe_himp, FirstOrder.Language.DefinableSet.coe_himp, TopologicalSpace.CompactOpens.coe_himp
|
ite 📖 | CompOp | 38 mathmath: PartialEquiv.piecewise_source, mulIndicator_preimage, subset_ite, ite_inter_closure_compl_eq_of_inter_frontier_eq, ite_empty_left, EqOn.piecewise_ite', ite_same, PartialEquiv.IsImage.leftInvOn_piecewise, MeasurableSet.ite, continuousOn_piecewise_ite', ite_compl, ite_right, ite_empty_right, ite_eq_of_subset_right, continuousOn_piecewise_ite, preimage_ite, PartialEquiv.piecewise_target, EqOn.piecewise_ite, ite_diff_self, inter_subset_ite, OpenPartialHomeomorph.IsImage.leftInvOn_piecewise, ite_subset_union, indicator_preimage, piecewise_preimage, ite_inter_compl_self, MapsTo.piecewise_ite, IsOpen.ite', ite_univ, ite_left, ite_inter_of_inter_eq, ite_eq_of_subset_left, IsOpen.ite, ite_empty, ite_inter_inter, ite_mono, ite_inter, ite_inter_self, ite_inter_closure_eq_of_inter_frontier_eq
|