Theorems · Theorem · convex and discrete geometry

ConvexCone.mk.inj

∀ {R : Type u_2} {M : Type u_4} {inst : Semiring R} {inst_1 : PartialOrder R} {inst_2 : AddCommMonoid M}
  {inst_3 : SMul R M} {carrier : Set M} {smul_mem' : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier → c • x ∈ carrier}
  {add_mem' : ∀ ⦃x : M⦄, x ∈ carrier → ∀ ⦃y : M⦄, y ∈ carrier → x + y ∈ carrier} {carrier_1 : Set M}
  {smul_mem'_1 : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier_1 → c • x ∈ carrier_1}
  {add_mem'_1 : ∀ ⦃x : M⦄, x ∈ carrier_1 → ∀ ⦃y : M⦄, y ∈ carrier_1 → x + y ∈ carrier_1},
  { carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' } =
      { carrier := carrier_1, smul_mem' := smul_mem'_1, add_mem' := add_mem'_1 } →
    carrier = carrier_1

Defined in

Mathlib.Geometry.Convex.Cone.Basic

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms