| Name | Category | Theorems |
|---|
IsFixedPt 📖 | MathDef | 28 mathmath: Tactic.ComputeAsymptotics.Seq.exists_fixed_point_of_contractible, isFixedPt_of_tendsto_iterate, Injective.isFixedPt_apply_iff, Polynomial.isFixedPt_newtonMap_of_isUnit_iff, minimalPeriod_eq_one_iff_isFixedPt, exists_mem_uIcc_isFixedPt, exists_mem_Icc_isFixedPt, isFixedPt_id, IsPeriodicPt.isFixedPt, OrderHom.isFixedPt_lfp, ContractingWith.exists_fixedPoint, mem_fixedPoints, ContractingWith.exists_fixedPoint', ContractingWith.efixedPoint_isFixedPt', minimalPeriod_eq_prime_iff, RootPairing.isFixedPt_reflection_of_isOrthogonal, isFixedPt_piMap, ODE.FunSpace.exists_isFixedPt_next, ContractingWith.efixedPoint_isFixedPt, forall_isFixedPt_iff, ContractingWith.fixedPoint_isFixedPt, Polynomial.isFixedPt_newtonMap_of_aeval_eq_zero, ContractingWith.isFixedPt_fixedPoint_iterate, isFixedPt_prodMap, exists_mem_Icc_isFixedPt_of_mapsTo, RootPairing.isFixedPt_reflectionPerm_iff, IsFixedPt.of_subsingleton, OrderHom.isFixedPt_gfp
|
dcomp 📖 | CompOp | 2 mathmath: MeasureTheory.lmarginal_image, FromTypes.curry_apply_cons
|
onFun 📖 | CompOp | 121 mathmath: Set.pairwise_disjoint_Ioc_zpow, Set.pairwise_disjoint_Ioo_add_zsmul, MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zero, Injective.pairwise_ne, Finset.pairwise_subtype_iff_pairwise_finset, Set.pairwise_disjoint_Ico_zsmul, Set.pairwise_disjoint_Ioo_mul_zpow, EmbeddingLike.pairwise_comp, Relation.onFun_map_onFun_iff_onFun, Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, MeasureTheory.pairwise_disjoint_fundamentalInterior, Nat.chineseRemainderOfList_nil, Antitone.pairwise_disjoint_on_Ioc_pred, exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, iSupIndep.pairwiseDisjoint, pairwise_disjoint_fiber, Antitone.pairwise_disjoint_on_Ioo_pred, pairwise_on_bool, pairwise_coprime_iff_coprime_prod, Set.pairwise_disjoint_Ioc_zsmul, Equiv.Perm.cycleFactorsFinset_eq_finset, RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, Monotone.pairwise_disjoint_on_Ioc_pred, Antitone.pairwise_disjoint_on_Ioo_succ, Set.pairwise_disjoint_Ioo_add_intCast, Set.pairwise_disjoint_vadd_iff, Finset.pairwise_cons', Set.pairwise_disjoint_Ioc_add_zsmul, Reflexive.comap, Multiset.nodup_bind, Set.pairwise_disjoint_Ioc_mul_zpow, Set.pairwise_disjoint_Ico_mul_zpow, Nat.pairwise_coprime_pow_primeFactors_factorization, Set.WellFoundedOn.mapsTo, Pairwise.comp_of_injective, Set.PairwiseDisjoint.aedisjoint, Set.pairwise_disjoint_Ico_add_intCast, LatticeCon.ker_r, Relation.map_onFun_eq_of_surjective, Symmetric.comap, exists_sum_eq_one_iff_pairwise_coprime', Relation.map_onFun_map_eq_map, EisensteinSeries.pairwise_disjoint_gammaSet, Relation.onFun_map_eq_of_injective, Submodule.IsMinimalPrimaryDecomposition.distinct, Set.wellFoundedOn_image, onFun_apply, Finset.pairwise_cons, Antitone.pairwise_disjoint_on_Ioc_succ, exists_seq_infinite_isOpen_pairwise_disjoint, BoxIntegral.Prepartition.pairwiseDisjoint, Set.InjOn.pairwise_image, Finset.disjiUnion_singleton, Set.pairwise_disjoint_Ioo_zpow, directedOn_onFun_iff, VitaliFamily.FineSubfamilyOn.covering_disjoint_subtype, List.nodup_flatMap, Set.pairwise_disjoint_Ioc_intCast, Set.pairwise_disjoint_Ioo_zsmul, Submodule.isPrimary_decomposition_pairwise_ne_radical, Valuation.Integers.wfDvdMonoid_iff_wellFounded_gt_on_v, IndexedPartition.disjoint, Set.pairwise_disjoint_Ioc_add_intCast, MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one, Monotone.pairwise_disjoint_on_Ico_pred, Metric.frontier_thickening_disjoint, Relation.map_onFun_le, Monotone.pairwise_disjoint_on_Ioo_succ, Relation.onFun_map_onFun_eq_onFun, Symmetric.pairwise_on, List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint, Monotone.pairwise_disjoint_on_Ioo_pred, Set.wellFoundedOn_range, Monotone.pairwise_disjoint_on_Ioc_succ, Set.pairwise_disjoint_Ico_zpow, Metric.frontier_cthickening_disjoint, Finset.pairwise_subtype_iff_pairwise_finset', Finset.disjiUnion_map, Fintype.exists_disjointed_le, MeasureTheory.IsFundamentalDomain.aedisjoint, Set.Pairwise.on_injective, WellFounded.onFun, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn, List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint, Bijective.pairwise_comp_iff, pairwise_disjoint_on_bool, injective_iff_pairwise_ne, orthogonalFamily_iff_pairwise, Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, Set.pairwise_disjoint_Ico_intCast, disjoint_disjointed, Set.pairwise_iff_exists_forall, subsingleton_setOf_mem_iff_pairwise_disjoint, ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal, Set.pairwise_disjoint_smul_iff, EquivLike.pairwise_comp_iff, Ideal.isPrimary_decomposition_pairwise_ne_radical, MeasureTheory.IsAddFundamentalDomain.aedisjoint, Antitone.pairwise_disjoint_on_Ico_pred, exists_sum_eq_one_iff_pairwise_coprime, pairwise_isRelPrime_iff_isRelPrime_prod, MeasureTheory.pairwise_disjoint_addFundamentalInterior, pairwise_disjoint_nhds, Relation.le_onFun_map, Set.pairwise_disjoint_Ico_add_zsmul, OrthogonalFamily.pairwise, iSupIndep_iff_pairwiseDisjoint, Polynomial.pairwise_coprime_X_sub_C, Transitive.comap, exists_seq_of_forall_finset_exists', Finset.disjiUnion_Iic_disjointed, Set.pairwise_disjoint_Ioo_intCast, TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover, NumberField.mixedEmbedding.disjoint_negAt_plusPart, List.pairwise_sublists, Equivalence.comap, pairwise_disjoint_on, Set.Nonempty.pairwise_iff_exists_forall, Antitone.pairwise_disjoint_on_Ico_succ, Monotone.pairwise_disjoint_on_Ico_succ
|
swap 📖 | CompOp | 92 mathmath: lowerPolar_swap, Relation.SymmGen.swap, Equiv.piComm_apply, Std.Antisymm.swap, RelHom.swap_apply, Relation.reflTransGen_swap, Computation.LiftRelAux.swap, IsAsymm.swap, Concept.swap_intent, Group.covariant_swap_iff_contravariant_swap, Primrec₂.swap, HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope, Ordinal.cof_type, incompRel_swap, Relation.ReflTransGen.swap, Relation.transGen_swap, Std.Total.swap, covariant_swap_add_of_covariant_add, equicontinuousWithinAt_iff_continuousWithinAt, swap_def, antisymmRel_swap_apply, IsPreorder.swap, Filter.covariant_swap_div, Std.Asymm.swap, Concept.swap_le_swap_iff, Concept.swap_extent, equicontinuousOn_iff_continuousOn, Computation.LiftRel.swap, IsStrictTotalOrder.swap, swap_ge, RelEmbedding.pairwise_swap_listMap, Concept.swap_swap, Concept.swapEquiv_apply, IsRefl.swap, equicontinuous_iff_continuous, contravariant_swap_mul_of_contravariant_mul, RelIso.pairwise_swap_listMap, AddGroup.covconv_swap, swap_hammingDist, Equiv.piComm_symm, swap_bijective, IsStrongAntichain.swap, HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope, List.rel_flatMap, Finset.bipartiteBelow_swap, Finset.bipartiteAbove_swap, uniformEquicontinuousOn_iff_uniformContinuousOn, incompRel_swap_apply, IsTrans.swap, IsAntichain.swap, Relation.symmGen_swap, Sigma.lex_swap, Concept.swap_lt_swap_iff, Relation.TransGen.swap, AddGroup.covariant_swap_iff_contravariant_swap, Equiv.functionSwap_apply, Relation.symmGen_swap_apply, IsStrictOrder.swap, Std.Refl.swap, swap_le, Std.Irrefl.swap, PrimrecRel.swap, Group.covconv_swap, contravariant_swap_add_of_contravariant_add, compRel_swap, equicontinuousAt_iff_continuousAt, List.Pairwise.sublists', IsPartialOrder.swap, Nat.Primrec.swap, Std.Trichotomous.swap, Equiv.functionSwap_symm_apply, swap_lt, RelEmbedding.sorted_swap_listMap, compRel_swap_apply, antisymmRel_swap, Concept.swapEquiv_symm_apply, covariant_swap_mul_of_covariant_mul, upperPolar_swap, Ordinal.principal_swap_iff, Nat.bitwise_swap, swap_dist, Stream'.WSeq.LiftRel.swap, IsTrichotomous.swap, Nat.Primrec.swap', Stream'.WSeq.LiftRelO.swap, swap_eq_iff, Stream'.WSeq.LiftRel.swap_lem, swap_gt, uniformEquicontinuous_iff_uniformContinuous, Filter.covariant_swap_sub, Symmetric.swap_eq, RelEmbedding.swap_apply
|
term_On_ 📖 | CompOp | — |
«term_∘'_» 📖 | CompOp | — |