| Name | Category | Theorems |
|---|
bihimp 📖 | CompOp | 76 mathmath: bihimp_left_involutive, bihimp_bihimp_cancel_right, bihimp_eq_left, codisjoint_bihimp_sup, IsCompl.bihimp_eq_bot, bihimp_bihimp_sup, inf_himp_bihimp, Codisjoint.bihimp_right, bihimp_right_surjective, bihimp_himp_left, bihimp_eq_right, bihimp_himp_eq_inf, top_bihimp, compl_symmDiff, Pi.bihimp_apply, Pi.bihimp_def, himp_bihimp_left, bihimp_left_comm, bihimp_left_surjective, bihimp_le_iff_left, bihimp_le_iff_right, bihimp_bihimp_self, MeasurableSet.bihimp, bihimp_triangle, bihimp_eq, bihimp_right_inj, bihimp_right_comm, bihimp_iff_iff, bihimp_eq_sup_himp_inf, bihimp_of_le, inf_le_bihimp, bihimp_comm, Codisjoint.bihimp_left, Codisjoint.bihimp_inf_bihimp_le_right, himp_bihimp_right, bihimp_of_ge, bihimp_inf_sup, bihimp_right_involutive, bihimp_eq_inf, bihimp_self, compl_bihimp_self, sup_bihimp_bihimp, bihimp_def, bihimp_left_inj, bihimp_left_injective, bihimp_bihimp_cancel_left, himp_bihimp_eq_inf, Codisjoint.bihimp_inf_bihimp_le_left, toDual_bihimp, sup_inf_bihimp, ofDual_symmDiff, map_bihimp, bot_bihimp, himp_bihimp, bihimp_bihimp_bihimp_comm, sup_himp_bihimp, ofDual_bihimp, toDual_symmDiff, compl_bihimp_compl, bihimp_fst, bihimp_isCommutative, bihimp_eq', bihimp_isAssociative, bihimp_hnot_self, compl_bihimp, bihimp_top, bihimp_snd, Codisjoint.bihimp_eq_inf, le_bihimp_iff, bihimp_eq_top, bihimp_bot, bihimp_himp_right, bihimp_assoc, le_bihimp, bihimp_eq_bot, bihimp_right_injective
|
symmDiff 📖 | CompOp | 194 mathmath: MeasureTheory.Measure.MeasureDense.approx, map_symmDiff', Pi.symmDiff_def, Set.inter_symmDiff_distrib_left, compl_symmDiff_self, symmDiff_def, Set.smul_set_symmDiff, ofBoolRing_sub, symmDiff_le, MeasureTheory.measureReal_symmDiff_le, symmDiff_eq', MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt, MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetRing, inf_symmDiff_distrib_right, Set.image_symmDiff, sdiff_symmDiff, Pi.symmDiff_apply, symmDiff_compl_self, Finset.symmDiff_eq_union_iff, MeasureTheory.measure_symmDiff_eq_top, symmDiff_symmDiff_self', Finset.Colex.toColex_lt_toColex_iff_max'_mem, Set.toFinset_symmDiff, symmDiff_top, hnot_symmDiff_self, Set.indicator_symmDiff, IsCompl.symmDiff_eq_top, Finset.Colex.le_iff_max'_mem, symmDiff_right_comm, Set.symmDiff_def, Disjoint.le_symmDiff_sup_symmDiff_right, symmDiff_top', MeasureTheory.measureReal_symmDiff_eq, symmDiff_of_ge, symmDiff_left_inj, disjoint_symmDiff_inf, top_symmDiff, symmDiff_assoc, sdiff_symmDiff', biSup_symmDiff_biSup_le, Finset.Colex.toColex_le_toColex_iff_max'_mem, Finset.smul_finset_symmDiff, Set.mem_symmDiff, beattySeq'_symmDiff_beattySeq_pos, IsAddFoelner.tendsto_meas_vadd_symmDiff_vadd, MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff', compl_symmDiff, ofBoolRing_add, IsFoelner.tendsto_meas_smul_symmDiff, symmDiff_fst, bot_symmDiff, SimpleGraph.Subgraph.IsPerfectMatching.isAlternating_symmDiff_left, MeasureTheory.Measure.MeasureDense.fin_meas_approx, MeasureTheory.edist_indicatorConstLp_eq_enorm, symmDiff_comm, symmDiff_sdiff_right, symmDiff_left_involutive, symmDiff_sdiff_left, Finset.vadd_finset_symmDiff, symmDiff_symmDiff_right, MeasureTheory.measure_symmDiff_le, MeasureTheory.measure_neg_vadd_symmDiff, symmDiff_right_inj, toBoolAlg_add, beattySeq_symmDiff_beattySeq'_pos, Irrational.beattySeq_symmDiff_beattySeq_pos, Set.union_symmDiff_subset, Finset.symmDiff_nonempty, symmDiff_snd, Disjoint.symmDiff_eq_sup, Finset.smul_finset_symmDiff₀, Set.Finite.toFinset_symmDiff, symmDiff_eq_right, symmDiff_eq, MeasureTheory.le_measure_symmDiff, symmDiff_eq_sup_sdiff_inf, Set.mulIndicator_symmDiff, MeasureTheory.measure_symmDiff_inv_smul, Finset.symmDiff_subset_sdiff, Finset.symmDiff_subset_union, symmDiff_eq_iff_sdiff_eq, dist_mulIndicator, symmDiff_sup_inf, symmDiff_self, le_symmDiff_iff_right, symmDiff_triangle, isFoelner_iff, ofBoolAlg_symmDiff, symmDiff_left_surjective, IsFoelner.tendsto_meas_smul_symmDiff_smul, Set.apply_indicator_symmDiff, Disjoint.le_symmDiff_sup_symmDiff_left, inf_symmDiff_distrib_left, symmDiff_isAssociative, Set.subset_symmDiff_union_symmDiff_right, Set.symmDiff_subset_union, MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero, symmDiff_isCommutative, nndist_mulIndicator, MeasureTheory.eLpNorm_indicator_sub_indicator, compl_symmDiff_compl, MeasurableSet.symmDiff, Filter.EventuallyEq.symmDiff, SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_isCycles, Set.Finite.symmDiff_congr, Set.inter_symmDiff_distrib_right, MeasureTheory.measure_inv_smul_symmDiff, Finset.coe_symmDiff, le_symmDiff_sup_left, symmDiff_sdiff, symmDiff_sdiff_eq_sup, symmDiff_le_sup, SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_of_isAlternating, symmDiff_symmDiff_left, symmDiff_symmDiff_cancel_left, symmDiff_eq_bot, Finset.Colex.lt_iff_max'_mem, Set.apply_mulIndicator_symmDiff, MeasureTheory.MeasuredSets.dist_def, Finset.symmDiff_subset_sdiff', le_symmDiff_iff_left, symmDiff_le_iff, inf_sup_symmDiff, symmDiff_eq_Xor', dist_indicator, symmDiff_right_surjective, le_symmDiff_sup_right, symmDiff_symmDiff_right', Set.Finite.symmDiff, MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff, Bool.symmDiff_eq_xor, MeasureTheory.measure_symmDiff_eq, Set.symmDiff_eq_empty, symmDiff_hnot_self, symmDiff_left_injective, MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative, toDual_bihimp, ofDual_symmDiff, Finset.symmDiff_eq_empty, symmDiff_eq_left, Set.mabs_mulIndicator_symmDiff, symmDiff_right_injective, symmDiff_eq_top, symmDiff_sdiff_inf, symmDiff_symmDiff_inf, MeasureTheory.ae_eq_set_symmDiff, MeasureTheory.measure_symmDiff_neg_vadd, symmDiff_of_le, sdiff_symmDiff_eq_sup, symmDiff_eq_sup, nndist_indicator, Finset.mem_symmDiff, IsAddFoelner.tendsto_meas_vadd_symmDiff, sdiff_symmDiff_left, Set.vadd_set_symmDiff, Set.symmDiff_nonempty, MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring, Set.preimage_symmDiff, symmDiff_left_comm, ofDual_bihimp, Set.subset_image_symmDiff, iSup_symmDiff_iSup_le, toDual_symmDiff, symmDiff_right_involutive, map_symmDiff, symmDiff_symmDiff_symmDiff_comm, Disjoint.symmDiff_right, MeasurableSet.exists_isOpen_symmDiff_lt, MvPolynomial.support_symmDiff_support_subset_support_add, MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le, Set.abs_indicator_symmDiff, top_symmDiff', inf_symmDiff_symmDiff, compl_bihimp, MeasureTheory.MeasuredSets.edist_def, MeasureTheory.measure_symmDiff_eq_zero_iff, symmDiff_symmDiff_cancel_right, symmDiff_bot, Finset.symmDiff_eq_union, edist_indicator, MeasureTheory.NullMeasurableSet.symmDiff, isAddFoelner_iff, toBoolRing_symmDiff, Disjoint.symmDiff_left, SimpleGraph.Subgraph.IsPerfectMatching.isAlternating_symmDiff_right, Set.smul_set_symmDiff₀, Set.symmDiff_union_subset, MeasureTheory.dist_indicatorConstLp_eq_norm, sdiff_symmDiff_right, Finset.image_symmDiff, Set.union_symmDiff_union_subset, sup_sdiff_symmDiff, edist_mulIndicator, Set.subset_symmDiff_union_symmDiff_left
|