Theorems · Theorem · convex and discrete geometry

ProperCone.map.congr_simp

∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : AddCommMonoid F]
  [inst_7 : TopologicalSpace F] [inst_8 : Module R F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul R F]
  (f f_1 : E →L[R] F), f = f_1 → ∀ (C C_1 : ProperCone R E), C = C_1 → ProperCone.map f C = ProperCone.map f_1 C_1

Defined in

Mathlib.Analysis.Convex.Cone.InnerDual

Cited by

0 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringPartialOrderIsOrderedRingAddCommMonoidTopologicalSpaceModuleAddCommMonoidTopologicalSpaceModuleContinuousAddContinuousConstSMul