Theorems · Theorem · convex and discrete geometry

ConvexCone.mk.injEq

∀ {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 19 from the axioms · uses propext

Assumes

SemiringPartialOrderAddCommMonoidSMul