Theorems · Theorem · convex and discrete geometry

Convexity.StdSimplex.restrict.congr_simp

∀ {X : Type u_2} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  (w w_1 : Convexity.StdSimplex K X) (e_w : w = w_1) (s s_1 : Set X) (e_s : s = s_1) (hs : ∃ x ∈ s, w.weights x ≠ 0),
  w.restrict s hs = w_1.restrict s_1 ⋯

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRing