Theorems · Definition · convex and discrete geometry

ConvexCone.mk.noConfusion

{R : Type u_2} →
  {M : Type u_4} →
    {inst : Semiring R} →
      {inst_1 : PartialOrder R} →
        {inst_2 : AddCommMonoid M} →
          {inst_3 : SMul R M} →
            {P : Sort u} →
              {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' : 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 := carrier, smul_mem' := smul_mem', add_mem' := add_mem' } =
                              { carrier := carrier', smul_mem' := smul_mem'', add_mem' := add_mem'' } →
                            (carrier ≍ carrier' → P) → P

Defined in

Mathlib.Geometry.Convex.Cone.Basic

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms