| Metric | Count |
|---|
DefinitionsHasUncurry, uncurry, decidableEq, Injective2, Involutive, IsPartialInv, bicompl, bicompr, decidableEqPFun, eval, extend, hasUncurryBase, hasUncurryInduction, invFun, partialInv, sometimes, surjInv, update, Β«termβΏ_Β», SeparatesPoints, piecewise, instDecidableCurryOfMk_mathlib, instDecidableUncurryOfFstSnd_mathlib | 23 |
Theoremsinvolutive_not, comp_left, comp_right, existsUnique, existsUnique_iff, injective, of_comp_iff, of_comp_iff', piMap, surjective, comp_left, comp_right, extend_apply, extend_comp, rfl, bijectiveβ_of_surjective, comp_left, dite, extend_apply, extend_comp, factorsThrough, hasLeftInverse, of_comp, of_comp_iff, of_comp_iff', of_comp_right, piMap, surjective_comp_right, surjective_comp_right', eq_iff, left, left', right, right', uncurry, bijective, comp_self, eq_iff, injective, ite_not, leftInverse, leftInverse_iff, rightInverse, surjective, cast_eq, comp, comp_eq_id, eq, eq_rec_eq, eq_rec_on_eq, eq_rightInverse, rightInverse, rightInverse_of_injective, rightInverse_of_surjective, surjective, comp, comp_eq_id, eq, injective, leftInverse, leftInverse_of_injective, leftInverse_of_surjective, bijectiveβ_of_injective, comp_left, exists, existsβ, existsβ, forall, forallβ, forallβ, hasRightInverse, injective_comp_right, of_comp, of_comp_iff, of_comp_iff', of_comp_left, piMap, right_cancellable, apply_extend, apply_invFun_apply, apply_update, apply_updateβ, bijective_iff_existsUnique, bijective_iff_has_inverse, bijective_of_subsingleton, cantor_injective, cantor_surjective, comp_surjInv, comp_update, const_def, const_inj, const_injective, curry_injective, curry_update, eq_update_iff, eq_update_self_iff, eval_apply, exists_update_iff, extend_apply', extend_comp, extend_const, extend_def, extend_id, extend_injective, factorsThrough_iff, flip_curry, forall_update_iff, funext_iff_of_subsingleton, hfunext, injective_comp_left_iff, injective_comp_right_iff_surjective, injective_iff_hasLeftInverse, injective_of_isPartialInv, injective_of_isPartialInv_right, injective_of_subsingleton, injective_surjInv, invFun_comp, invFun_eq, invFun_eq_of_injective_of_rightInverse, invFun_neg, invFun_surjective, isPartialInv_left, leftInverse_iff_comp, leftInverse_invFun, leftInverse_surjInv, ne_iff, ne_update_self_iff, not_bijective, not_injective, not_injective_iff, not_involutive, not_surjective, not_surjective_Type, onFun_apply, partialInv_left, partialInv_of_injective, pred_update, rec_update, rightInverse_iff_comp, rightInverse_invFun, rightInverse_surjInv, sometimes_eq, sometimes_spec, surjInv_eq, surjective_comp_left_iff, surjective_comp_right_iff_injective, surjective_eval, surjective_iff_hasRightInverse, surjective_of_right_cancellable_Prop, surjective_to_subsingleton, swap_ge, swap_gt, swap_le, swap_lt, symmetric_apply_eq_iff, uncurry_bicompl, uncurry_bicompr, uncurry_def, uncurry_flip, uncurry_injective, uncurry_update_update, update_apply, update_apply_of_injective, update_comm, update_comp_eq_of_forall_ne, update_comp_eq_of_forall_ne', update_comp_eq_of_injective, update_comp_eq_of_injective', update_eq_const_of_subsingleton, update_eq_iff, update_eq_self, update_eq_self_iff, update_idem, update_injective, update_ne_self_iff, update_of_ne, update_self, equivalence, rec_update, map_comp_map, map_id, map_id', map_injective, map_update, forall_existsUnique_iff, forall_existsUnique_iff', cast_bijective, cast_inj, eq_mp_bijective, eq_mpr_bijective, eq_rec_inj, eq_rec_on_bijective, forall_existsUnique_iff, forall_existsUnique_iff' | 194 |
| Total | 217 |
| Name | Category | Theorems |
|---|
HasUncurry π | CompData | β |
Injective2 π | MathDef | 9 mathmath: Stream'.Seq.cons_injective2, ZFSet.pair_injective, Fin.insertNth_injective2, Stream'.cons_injective2, Finset.Injective2_disjSum, Fin.cons_injective2, Matrix.fromCols_inj, Matrix.fromRows_inj, Fin.snoc_injective2
|
Involutive π | MathDef | 55 mathmath: AffineIsometryEquiv.pointReflection_involutive, const_sub_involutive, bihimp_left_involutive, RootPairing.reflectionPerm_involutive, Fin.rev_involutive, FreeAddGroup.negRev_involutive, Equiv.divLeft_involutive, Equiv.swap_smul_involutive, InvolutiveStar.star_involutive, Bool.involutive_not, not_involutive, NumberField.ComplexEmbedding.involutive_conjugate, EuclideanGeometry.inversion_involutive, FreeGroup.invRev_involutive, SimpleGraph.Dart.symm_involutive, symmDiff_left_involutive, AffineEquiv.pointReflection_involutive, Equiv.pointReflection_involutive, Equiv.swap_mul_involutive, Composition.reverse_involutive, involutive_iff_iter_2_eq_id, Prod.map_involutive, Module.involutive_reflection, Polynomial.mirror_involutive, Equiv.mul_swap_involutive, FractionalIdeal.dual_involutive, ContextFreeGrammar.reverse_involutive, Symmetric.forall_existsUnique_iff', inv_involutive, Matroid.dual_involutive, Symmetric.forall_existsUnique_iff, bihimp_right_involutive, LinearMap.BilinForm.dualBasis_involutive, compl_involutive, conjneg_involutive, Module.Basis.traceDual_involutive, Equidecomp.symm_involutive, const_div_involutive, Fin2.rev_involutive, List.map_involutive_iff, Submodule.reflection_involutive, neg_involutive, EuclideanGeometry.reflection_involutive, Language.reverse_involutive, List.reverse_involutive, CliffordAlgebra.involute_involutive, ContextFreeRule.reverse_involutive, Quandle.dihedralAct.inv, symmDiff_right_involutive, unitInterval.symm_involutive, symmetric_apply_eq_iff, Module.involutive_preReflection, Equiv.subLeft_involutive, CliffordAlgebra.reverse_involutive, LaurentPolynomial.involutive_invert
|
IsPartialInv π | MathDef | 2 mathmath: partialInv_of_injective, Encodable.decodeβ_is_partial_inv
|
bicompl π | CompOp | 5 mathmath: uncurry_bicompl, Semiconjβ.comp_eq, bicompl.lawfulBifunctor, instLawfulBitraversableBicomplOfLawfulTraversable, UniformContinuousβ.bicompl
|
bicompr π | CompOp | 5 mathmath: UniformContinuousβ.comp, instLawfulBitraversableBicomprOfLawfulTraversable, Semiconjβ.comp_eq, bicompr.lawfulBifunctor, uncurry_bicompr
|
decidableEqPFun π | CompOp | β |
eval π | CompOp | 75 mathmath: Pi.uniformSpace_eq, cauchy_pi_iff', monotone_eval, isOpenMap_eval, Set.univ_pi_eq_iInter, Set.eval_image_pi_subset, Bornology.isVonNBounded_pi_iff, UniformOnFun.uniformContinuous_eval, MeasureTheory.Measure.pi_eval_preimage_null, Set.singleton_pi, surjective_eval, Set.eval_preimage, Pi.uniformSpace_comap_precomp, Set.pi_diff_pi_subset, Set.forall_finite_image_eval_iff, Set.eval_image_univ_pi_subset, Pi.induced_restrict, Pi.uniformSpace_comap_restrict, sphere_pi, bddAbove_pi, Filter.compl_mem_coprodα΅’, Pi.isCompact_closure_iff, Pi.uniformSpace_comap_precomp', Pi.coe_evalLatticeHom, Filter.mem_coprodα΅’_iff, MeasureTheory.measurePreserving_eval, Filter.mem_pi_of_mem, MeasureTheory.Measure.pi_map_eval, LinearMap.coe_proj, Filter.comap_eval_neBot, isGLB_pi, Real.volume_pi_le_prod_diam, Filter.comap_eval_neBot_iff, Bornology.forall_isBounded_image_eval_iff, measurePreserving_eval_infinitePi, OrderHom.apply_coe, Pi.induced_precomp, Set.subset_eval_image_pi, Set.eval_image_pi_of_notMem, Pi.evalMulActionHom_apply, Set.insert_pi, MeasureTheory.Measure.quasiMeasurePreserving_eval, Pi.isCompact_iff, LinearEquiv.funUnique_apply, LipschitzWith.eval, Pi.coe_evalMonoidHom, UniformOnFun.uniformContinuous_eval_of_mem_sUnion, Pi.exists_compact_superset_iff, bddBelow_pi, cauchy_pi_iff, MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton, UniformFun.uniformContinuous_eval, eval_apply, Pi.evalAddActionHom_apply, Filter.map_eval_pi, Set.univ_pi_update_univ, Set.eval_image_pi, Pi.induced_precomp', MeasureTheory.piPremeasure_pi_eval, MeasureTheory.Measure.tendsto_eval_ae_ae, Pi.isCompact_iff_of_isClosed, Pi.evalOrderHom_coe, Set.pi_def, ContinuousMap.eval_apply, Set.range_eval, Bornology.IsBounded.image_eval, MeasurableSpace.pi_eq_generateFrom_projections, UniformOnFun.uniformContinuous_eval_of_mem, isLUB_pi, Filter.tendsto_eval_pi, Set.subset_pi_eval_image, Filter.comap_eval_neBot_iff', Filter.le_pi, ContinuousLinearEquiv.coe_funUnique, Set.eval_preimage'
|
extend π | CompOp | 71 mathmath: AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq, ExtendByOne.hom_apply, HasCompactMulSupport.mulTSupport_extend_one_subset, Finset.prod_eq_prod_extend, extend_const, OpenPartialHomeomorph.lift_openEmbedding_toFun, extend_nonpos, tprod_extend_one, extend_add, HasCompactMulSupport.mulTSupport_extend_one, extend_val_apply', Set.restrict_extend_range, Embedding.arrowCongrLeft_apply, extend_neg, FactorsThrough.extend_apply, extend_injective, extend_vadd, Pairwise.disjoint_extend_bot, Directed.extend_bot, extend_def, extend_id, support_extend_zero_subset, FactorsThrough.extend_comp, tsum_extend_zero, apply_extend, Injective.extend_apply, HasCompactMulSupport.extend_one, Set.range_extend_subset, hasSum_extend_zero, ContMDiff.extend_zero, mulSupport_extend_one_subset, MeasurableEmbedding.stronglyMeasurable_extend, cfcβHom_eq_cfcβ_extend, extend_one, one_le_extend, HasCompactSupport.tsupport_extend_zero_subset, extend_zero, cfcHom_eq_cfc_extend, HasCompactSupport.continuous_extend_zero, extend_le_one, extend_mul, Set.restrict_extend_compl_range, extend_comp, AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype, iInf_extend_top, ExtendByZero.hom_apply, HasCompactSupport.extend_zero, support_extend_zero, extend_apply', MeasurableEmbedding.measurable_extend, extend_inv, extend_nonneg, mulSupport_extend_one, ExtendByZero.linearMap_apply, HasCompactSupport.tsupport_extend_zero, extend_val_apply, ContMDiff.extend_one, HasCompactMulSupport.continuous_extend_one, Equiv.extend_apply, extend_of_isEmpty, multipliable_extend_one, Injective.extend_comp, extend_smul, extend_div, summable_extend_zero, iSup_extend_bot, extend_sub, Set.range_extend, Finset.sum_eq_sum_extend, hasProd_extend_one, MeasureTheory.Measure.sum_extend_zero
|
hasUncurryBase π | CompOp | 6 mathmath: tendsto_prod_filter_iff, tendsto_prod_top_iff, Path.continuous_uncurry_extend_of_continuous_family, Filter.Tendsto.pathExtend, Filter.Tendsto.curry, tendsto_prod_principal_iff
|
hasUncurryInduction π | CompOp | 6 mathmath: tendsto_prod_filter_iff, tendsto_prod_top_iff, Path.continuous_uncurry_extend_of_continuous_family, Filter.Tendsto.pathExtend, Filter.Tendsto.curry, tendsto_prod_principal_iff
|
invFun π | CompOp | 17 mathmath: ModuleCat.linearIndependent_shortExact, Set.preimage_invFun_of_mem, rightInverse_invFun, invFun_comp, invFun_surjective, AkraBazziRecurrence.p_def, apply_invFun_apply, Embedding.invFun_restrict, leftInverse_invFun, invFun_eq_of_injective_of_rightInverse, Set.preimage_invFun_of_notMem, invFun_neg, ModuleCat.span_rightExact, Injective.invFun_restrict, invFun_eq, AddMonoidAlgebra.supDegree_mem_support, AddMonoidAlgebra.apply_supDegree_add_supDegree
|
partialInv π | CompOp | 2 mathmath: partialInv_of_injective, partialInv_left
|
sometimes π | CompOp | 2 mathmath: sometimes_spec, sometimes_eq
|
surjInv π | CompOp | 14 mathmath: Topology.IsQuotientMap.homeomorph_symm_apply, Algebra.PreSubmersivePresentation.ofHasCoeffs_Ο', FiniteField.frobeniusAlgEquiv_symm_apply, CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_symm_apply, FiniteField.frobeniusAlgEquivOfAlgebraic_symm_apply, IsHomeomorph.homeomorph_symm_apply, surjInv_eq, comp_surjInv, rightInverse_surjInv, CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_symm_apply, IsGaloisGroup.mulEquivAlgEquiv_symm_apply, SemidirectProduct.mulEquivSubgroup_symm_apply, injective_surjInv, leftInverse_surjInv
|
update π | CompOp | 317 mathmath: update_eq_updateFinset, update_lt_update_iff, Pi.update_eq_div_mul_mulSingle, update_apply_of_injective, apply_update, Finset.piecewise_insert, Set.piecewise_insert, Fin.init_update_last, MultilinearMap.map_update_smul, MultilinearMap.map_update_add, BoxIntegral.Box.splitLower_def, Pi.image_update_openSegment, Nat.binomial_succ_succ, update_eq_self, le_update_self_iff, ContinuousMultilinearMap.map_update_sub, PiTensorProduct.subsingletonEquiv_symm_apply, update_mono, Finset.set_biUnion_insert_update, update_strictMono, Set.piecewise_singleton, Equiv.comp_swap_eq_update, measurable_update', Set.image_update_Ioo, update_inf, Pi.covBy_iff_exists_right_eq, update_eventuallyEq_nhdsNE, MeasureTheory.lintegral_prod_lintegral_pow_le, MeasureTheory.measurable_update_cylinderEvents, AlternatingMap.map_update_smul, Sum.update_inl_apply_inl, Affine.Simplex.affineIndependent_points_update_centroid, Sum.update_inr_apply_inr', MultilinearMap.map_update, PiNat.update_mem_cylinder, Finset.set_biInter_insert_update, Sigma.curry_update, update_exp, Summable.update, Matrix.diagonal_updateRow_single, ContinuousMultilinearMap.linearDeriv_apply, Fintype.piFinset_update_eq_filter_piFinset_mem, Set.disjoint_pi_univ_Ioc_update_left_right, dite_comp_equiv_update, Set.eval_preimage, update_updateFinset, PiTensorProduct.mapL_smul, update_eq_iff, ProbabilityTheory.Kernel.le_lmarginalPartialTraj_succ, MultilinearMap.map_update_add', piCongrLeft'_symm_update, update_le_update_iff', dslope_sub_smul, TopologicalSpace.nhds_mkOfNhds_single, Pi.toLex_update_le_self_iff, MeasureTheory.measurable_update_cylinderEvents_left, PiNat.iUnion_cylinder_update, BoxIntegral.Box.splitUpper_def, Pi.toLex_update_lt_self_iff, update_one, update_smul, Set.image_update_Icc, Matrix.vecMulVec_update, comp_update, List.Nodup.map_update, Complex.differentiableOn_update_limUnder_of_isLittleO, Set.update_mem_pi_iff, Complex.differentiableOn_update_limUnder_of_bddAbove, Filter.Tendsto.update, Set.image_update_Ico_right, support_update_of_ne_zero, ContinuousMultilinearMap.map_update_add, update_comp_eq_of_notMem_range, update_le_update_iff, AlternatingMap.map_update_add, Set.image_update_Icc_left, Fintype.piFinset_update_singleton_eq_filter_piFinset_eq, updateFinset_singleton, Pi.le_toLex_update_self_iff, Turing.PartrecToTM2.move_ok, contDiff_update, ContinuousAlternatingMap.map_update_sub, update_comp_equiv, ULift.rec_update, MeromorphicOn.meromorphicTrailingCoeffAt_extract_zeros_poles, ContinuousAlternatingMap.map_update_add, Sum.update_inl_apply_inl', MeasureTheory.lintegral_mul_prod_lintegral_pow_le, Polynomial.idealSpan_range_update_divByMonic, Turing.PartrecToTM2.K'.elim_update_main, mulSupport_update_one, update_comp_eq_of_notMem_range', Finset.update_eq_piecewise, hasDerivAt_update, nhds_nhdsAdjoint, Set.pi_update_of_notMem, Finsupp.single_eq_update, MultilinearMap.map_update_smul_left, AlternatingMap.map_update_zero, MeasureTheory.lmarginal_erase, Set.pi_univ_Ioc_update_right, Option.rec_update, Set.Icc_diff_pi_univ_Ioc_subset, MeasureTheory.lmarginal_insert, MeasureTheory.lmarginal_singleton, ContinuousAlternatingMap.map_update_smul, Fin.removeNth_update_succAbove, update_apply, update_eq_const_of_subsingleton, MultilinearMap.map_update_neg, update_inv, DependsOn.update, measurable_update_left, Fin.snoc_update, update_eventuallyEq, Matrix.diagonal_updateCol_single, Set.Icc_diff_pi_univ_Ioo_subset, isClosedEmbedding_update, Fin.update_insertNth, mulSupport_update_of_ne_one, AlternatingMap.map_update_sum, Fin.update_cons_zero, HasSum.update, MeasureTheory.measurable_update_cylinderEvents', AlternatingMap.map_update_update, ContinuousMultilinearMap.toContinuousLinearMap_apply, MeasureTheory.lmarginal_erase', lt_update_self_iff, Set.update_preimage_univ_pi, update_comp_eq_of_forall_ne, Pi.lt_toColex_update_self_iff, Set.update_image, continuousOn_update_iff, MultilinearMap.map_update_sub, Finsupp.coe_update, eq_update_self_iff, piCongrLeft'_update, Set.update_mem_pi_iff_of_mem, ContinuousAt.update, deriv_update, update_comm, Sum.update_inr_comp_inl, Continuous.update, Turing.PartrecToTM2.K'.elim_update_stack, MeromorphicAt.update_iff, MultilinearMap.map_update_zero, MultilinearMap.iteratedFDeriv_aux, MeromorphicAt.update, eq_update_iff, fderiv_update, MultilinearMap.map_update_smul', PiTensorProduct.smul_tprodCoeff_aux, Fin.take_update_of_ge, Finset.prod_update_of_notMem, DFinsupp.coe_update, update_comp_eq_of_forall_ne', AlternatingMap.map_update_neg, Set.image_update_Ioc_right, le_update_iff, Submodule.span_range_update_sub_smul, update_vadd, Pi.isAtom_iff_eq_single, Sum.update_inr_apply_inr, continuous_update, MultilinearMap.domDomRestrict_aux, Equiv.swap_eq_update, fderiv_continuousAlternatingMap_apply_apply, Finset.iInf_insert_update, Sum.update_inr_apply_inl, hasFDerivAt_update, FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational, exteriorPower.presentation_relation, Pi.wcovBy_iff_exists_left_eq, Finset.update_piecewise_of_notMem, Sum.rec_update_left, Fin.removeNth_update, HurwitzZeta.differentiableAt_update_of_residue, forall_update_iff, Set.image_update_Ioc_left, rec_update, update_zero, pred_update, fderivWithin_continuousAlternatingMap_apply_apply, Submodule.span_range_update_add_smul, Fin.insertNth_update, Finset.sum_update_of_notMem, MultilinearMap.domDomRestrict_aux_right, Set.pi_univ_Ioc_update_union, Finset.sum_update_of_mem, AlternatingMap.map_update_sub, Matrix.update_vecMulVec, Pi.lt_toLex_update_self_iff, Finset.piecewise_singleton, update_idem, update_le_iff, Set.univ_pi_update, Finset.update_piecewise, update_eq_self_iff, update_injective, Sum.update_inl_comp_inl, Module.Basis.toMatrix_update, PiTensorProduct.smul_tprodCoeff, continuousAt_update_of_ne, ContinuousMultilinearMap.map_update_smul, Set.image_update_uIcc_left, AlternatingMap.map_update_self, Sum.update_elim_inl, mulSupport_update_eq_ite, Finset.iSup_insert_update, update_star, Sum.elim_update_left, Pi.toColex_update_le_self_iff, OrderedFinpartition.extendMiddle_partSize, Fin.update_snoc_last, LinearMap.update_apply, Finset.piecewise_erase_univ, Pi.covBy_iff_exists_left_eq, ContinuousAlternatingMap.fderivCompContinuousLinearMap_apply, Fin.init_update_castSucc, Pi.map_update, PiTensorProduct.add_tprodCoeff, Multipliable.update, Sum.rec_update_right, FactorizedRational.extractFactor, Set.image_update_Ico_left, Sum.update_elim_inr, Set.update_preimage_pi, HasDerivAt.continuousAt_div, Fin.tail_update_succ, OrderedFinpartition.applyOrderedFinpartition_update_left, Fin.tail_update_zero, MeasureTheory.lmarginal_update_of_notMem, support_update_eq_ite, Set.pi_univ_Ioc_update_left, Set.image_update_uIcc, Turing.PartrecToTM2.clear_ok, Set.image_update_uIcc_right, Polynomial.coeff_update, update_neg, ContinuousAlternatingMap.map_update_zero, Fin.insertNth_removeNth, Pi.update_eq_sub_add_single, Sum.update_inr_comp_inr, Turing.PartrecToTM2.moveβ_ok, ContinuousAlternatingMap.toContinuousLinearMap_apply, Set.image_update_Ico, Pi.image_update_segment, curry_update, HasProd.update, Set.univ_pi_update_univ, Complex.differentiableOn_update_limUnder_insert_of_isLittleO, Sum.elim_update_right, Matrix.single_mulVec, PiTensorProduct.map_update_smul, Pi.le_toColex_update_self_iff, MultilinearMap.linearDeriv_apply, update_comp_eq_of_injective, Pi.wcovBy_iff_exists_right_eq, MultilinearMap.toLinearMap_apply, continuousWithinAt_update_of_ne, update_self, Matrix.updateRow_mulVec, FormalMultilinearSeries.applyComposition_update, Matrix.vecMul_updateCol, update_lt_self_iff, update_le_self_iff, PiTensorProduct.map_update_add, MeasureTheory.GridLines.T_univ, apply_updateβ, Set.image_update_Ioc, continuousWithinAt_update_same, Module.Basis.orientation_neg_single, ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply, update_sub, Sum.update_inl_apply_inr, Set.image_update_Ioo_left, uncurry_update_update, update_add, update_div, update_mul, ProbabilityTheory.Kernel.lmarginalPartialTraj_succ, PiTensorProduct.mapL_add, Turing.PartrecToTM2.unrev_ok, Nat.succ_mul_binomial, Set.pi_update_of_mem, update_comp_eq_of_injective', update_apply_equiv_apply, WithZeroTopology.nhds_eq_update, Finset.update_piecewise_of_mem, support_update_zero, OrderedFinpartition.applyOrderedFinpartition_update_right, update_eventuallyEq_cofinite, update_sup, Fin.take_update_of_lt, SkewMonoidAlgebra.coeff_update, Finset.prod_update_of_mem, exteriorPower.presentation.relations_relation, MeasureTheory.lmarginal_update_of_mem, continuousAt_update_same, MultilinearMap.map_update_sum, Fin.cons_update, Set.image_update_Ioo_right, Sum.update_inl_comp_inr, Turing.TM2to1.tr_respects_auxβ, Turing.TM2to1.step_run, Set.image_update_Icc_right, Turing.PartrecToTM2.K'.elim_update_rev, Pi.toColex_update_lt_self_iff, AffineIndependent.affineIndependent_update_of_notMem_affineSpan, Turing.PartrecToTM2.K'.elim_update_aux, Option.elim'_update, Set.eval_preimage', MeasureTheory.lmarginal_insert', Pi.isAtom_single, measurable_update, update_of_ne, exists_update_iff
|
Β«termβΏ_Β» π | CompOp | β |