An Oriented Cap Edge Is a Two-Element Subset
ProvedProblem97.CGN.edgeAt_mem_powersetCardcap-edgeconvex-geometryerdos-97-96-countingfinsetlean-formalization
If every vertex of an ordered cap L lies in a finite set A and r < s, then the unordered edge formed by L(r) and L(s) is a two-element subset of A, hence belongs to the two-element powerset of A.
Preamble
/- Generated theorem stub from Erdos9796Proof.P97.CGN.CGN by Stage 2 proof cut; source SHA-256 9f1ccd7df30637d7fbdf412fb40177dedb5193c45ec2993df86f137cbd34ffb7 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_CGN_CGN
import Definitions.Def_Erdos9796Counting_Foundation
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Order.Interval.Finset.Fin
open Problem97 Problem97.CGN
/-!
# CGN7: indexed cap-side witness matching scaffold
This file records the CGN7-local indexed witness relation requested by the
updated counterexample-card-ge-nine prose. The geometry that produces the
one-sided injectivity hypotheses lives in the CGN6 lemmas; this module only
packages the ordered-cap interface and the partial-matching counting shell.
-/
open scoped EuclideanGeometry
open scoped InnerProductSpace
open Finset
variable {m : ℕ}Formal statement
theorem Problem97.CGN.edgeAt_mem_powersetCard {m : ℕ} {A : Finset ℝ²} (L : OrderedCap m)
(hmem : ∀ t : Fin m, L.points t ∈ A) {r s : Fin m} (hrs : r < s) :
edgeAt L r s ∈ A.powersetCard 2 := by sorrySource