Structures · Analysis
IsRCLikeNormedField
A mixin over a normed field, saying that the norm field structure is the same as ℝ or ℂ.
To endow such a field with a compatible RCLike structure in a proof, use
letI := IsRCLikeNormedField.rclike 𝕜.
- Defined in
- Mathlib.Analysis.RCLike.Basic
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by85
- IsRCLikeNormedField.rclike
- Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
- implicitFunctionOfBivariate
- hasStrictFDerivAt_uncurry_coprod
- Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
- summable_of_summable_hasFDerivAt_of_isPreconnected
- IsOpen.exists_is_const_of_fderiv_eq_zero
- Convex.eqOn_of_fderivWithin_eq
- hasFDerivAt_tsum_of_isPreconnected
- hasDerivAt_of_tendstoLocallyUniformlyOn
- Convex.is_const_of_fderivWithin_eq_zero
- IsOpen.isOpen_inter_preimage_of_fderiv_eq_zero
- Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le'
- iteratedFDeriv_tsum
- hasFDerivAt_of_tendstoLocallyUniformlyOn
- hasFDerivAt_tsum
- UniqueDiffWithinAt.of_real
- hasFDerivAt_of_tendstoUniformlyOn
- minSmoothness_of_isRCLikeNormedField
- differentiable_tsum
- Module.Dual.exists_continuous_extension_of_le_seminorm
- second_derivative_symmetric_of_eventually
- uniformCauchySeqOn_ball_of_fderiv
- hasFDerivAt_of_tendstoUniformlyOnFilter
- Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt
- IsOpen.exists_eq_add_of_fderiv_eq
- hasDerivAt_of_tendstoUniformlyOnFilter
- contDiff_tsum
- uniformCauchySeqOnFilter_of_fderiv
- contDiff_tsum_of_eventually
- hasDerivAt_tsum_of_isPreconnected
- summable_of_summable_hasDerivAt_of_isPreconnected
- derivWithin_tsum
- lipschitzWith_of_nnnorm_fderiv_le
- uniqueDiffOn_convex_of_isRCLikeNormedField
- UniqueDiffOn.of_real
- Module.Dual.exists_extension_of_le_seminorm
- cauchy_map_of_uniformCauchySeqOn_fderiv
- hasDerivAt_of_tendstoUniformlyOn
- deriv_tsum_apply
- hasDerivAt_of_tendsto_locally_uniformly_on'
- Convex.norm_image_sub_le_of_norm_fderivWithin_le
- exists_extension_norm_eq
- iteratedDerivWithin_tsum
- fderiv_tsum
- Convex.norm_image_sub_le_of_norm_fderivWithin_le'
- Convex.lipschitzOnWith_of_nnnorm_fderiv_le
- IsOpen.is_const_of_fderiv_eq_zero
- fderiv_tsum_apply
- Convex.norm_image_sub_le_of_norm_fderiv_le
Ancestors0
No ancestors.