Theorems · Theorem · convex and discrete geometry

Geometry.SimplicialComplex.convexHull_inter_convexHull

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s t : Finset E},
  s ∈ K.faces → t ∈ K.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) (↑s ∩ ↑t)

Defined in: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring PartialOrder AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
Setstatement · cited by 53,352
Modulestatement and proof · cited by 20,661
Finsetstatement and proof · cited by 13,712
AddCommGroupstatement and proof · cited by 12,871
SetLike.coestatement · cited by 8,199
Ringstatement and proof · cited by 7,463
PartialOrderstatement and proof · cited by 6,410
LE.le.antisymmproof · cited by 507
ClosureOperatorstatement · cited by 371
Set.inter_subset_leftproof · cited by 360
Set.inter_subset_rightproof · cited by 329

Cited by1

Results whose statement or proof uses this declaration.

Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHullproof · cited by 0