Theorems · Theorem · functional analysis
ContinuousLinearMap.toSpanSingleton.congr_simp
∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
[inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁] (x x_1 : M₁),
x = x_1 → ContinuousLinearMap.toSpanSingleton R₁ x = ContinuousLinearMap.toSpanSingleton R₁ x_1- Cited by
- 12 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- ContinuousLinearMapstatement · cited by 5,352
- ContinuousSMulstatement and proof · cited by 1,016
- ContinuousLinearMap.toSpanSingletonstatement and proof · cited by 133
Cited by12
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.toSpanSingleton_powproof · cited by 3
- is_const_of_deriv_eq_zeroproof · cited by 2
- hasFDerivAt_stereoInvFunAuxproof · cited by 1
- IsOpen.exists_is_const_of_deriv_eq_zeroproof · cited by 1
- Filter.EventuallyEq.hasDerivAtFilter_iffproof · cited by 1
- UpperHalfPlane.smulFDeriv_J_mulproof · cited by 1
- IsOpen.exists_eq_add_of_deriv_eqproof · cited by 0
- Convex.exists_forall_hasDerivWithinAtproof · cited by 0
- IsOpen.isOpen_inter_preimage_of_deriv_eq_zeroproof · cited by 0
- IsOpen.is_const_of_deriv_eq_zeroproof · cited by 0
- UpperHalfPlane.hasStrictFDerivAt_smulproof · cited by 0
- UpperHalfPlane.det_smulFDerivproof · cited by 0