MathlibAnnex/Analysis/Normed/GeometricStructure/Face.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6module78public import Mathlib.Analysis.Convex.Extreme9public import Mathlib.Analysis.Normed.Module.Dual1011/-!12# Maximal proper real convex faces of the closed unit ball1314`IsExtreme` is the existing Mathlib extreme-subset predicate. Convexity is a15separate requirement. Maximality is among proper convex faces. In particular,16exposedness, supporting-functional existence, compactness, and extreme supporting17functionals are not fields of the predicate.18-/1920@[expose] public section2122set_option autoImplicit false2324universe u2526namespace NormedSpace2728variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]2930/-- A nonempty proper real convex face, maximal among the proper real convex faces31of the closed unit ball. -/32structure IsMaximalFace (F : Set E) : Prop where33  nonempty : F.Nonempty34  convex : Convex ℝ F35  isExtreme : IsExtreme ℝ (Metric.closedBall (0 : E) 1) F36  ne_closedBall : F ≠ Metric.closedBall (0 : E) 137  maximal : ∀ G : Set E, F ⊆ G → Convex ℝ G →38    IsExtreme ℝ (Metric.closedBall (0 : E) 1) G →39    G ≠ Metric.closedBall (0 : E) 1 → G = F4041theorem IsMaximalFace.subset_closedBall {F : Set E} (hF : IsMaximalFace F) :42    F ⊆ Metric.closedBall (0 : E) 1 := hF.isExtreme.subset4344/-- The zero space has no nonempty proper maximal face. -/45theorem not_isMaximalFace_of_subsingleton [Subsingleton E] (F : Set E) :46    ¬ IsMaximalFace F := by47  intro hF48  apply hF.ne_closedBall49  apply Set.Subset.antisymm hF.subset_closedBall50  obtain ⟨x, hx⟩ := hF.nonempty51  intro y _52  exact (Subsingleton.elim x y) ▸ hx5354end NormedSpace