Theorems · Theorem · convex and discrete geometry

image_extremePoints

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {L : Type u_6} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜]
  [IsOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F]
  [inst_7 : EquivLike L E F] [LinearEquivClass L 𝕜 E F] (f : L) (s : Set E),
  ⇑f '' Set.extremePoints 𝕜 s = Set.extremePoints 𝕜 (⇑f '' s)

Defined in

Mathlib.Analysis.Convex.Extreme

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingPartialOrderIsOrderedRingAddCommGroupModuleAddCommGroupModuleEquivLikeLinearEquivClass