From d9b6f74b6576524546d1b9ab73cf2d523fe60fcd Mon Sep 17 00:00:00 2001 From: VTC Date: Wed, 27 May 2026 16:02:52 +0200 Subject: [PATCH 01/11] changes from covexspace to convexity --- .../LinearAlgebra/Face/Basic copy.lean | 149 ++++++++++++++++++ .../Mathlib/LinearAlgebra/Face/Basic.lean | 149 ++++++++++++++++++ 2 files changed, 298 insertions(+) create mode 100644 Polyhedral/Mathlib/LinearAlgebra/Face/Basic copy.lean create mode 100644 Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic copy.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic copy.lean new file mode 100644 index 00000000..5bdeeff5 --- /dev/null +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic copy.lean @@ -0,0 +1,149 @@ +import Polyhedral.Mathlib.LinearAlgebra.ConvexSpace +import Mathlib.Analysis.Convex.Segment + + +open ConvexSpace + +namespace ConvexSet + +variable (R : Type*) {M : Type*} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] + [ConvexSpace R M] + +theorem refl (S : ConvexSet R M) : S.IsFaceOf S := by + constructor + · simp + · intro x hx y hy z hz h + apply hx + +theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by + unfold ConvexSpace.openSegment + ext z + apply Iff.intro + · intro h + simp only [Set.mem_setOf_eq] + rcases h with ⟨m, n, hm , hn , hmn , hz⟩ + use n, m, hn, hm + rw [add_comm] at hmn + use hmn + unfold convexComboPair + unfold convexCombination + sorry + · intro h + simp only [Set.mem_setOf_eq] + rcases h with ⟨m,n,hm,hn,hmn,hz⟩ + use n,m,hn,hm + rw [add_comm] at hmn + sorry + +theorem trans (S F₁ F₂ : ConvexSet R M) (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf S) : +F₂.IsFaceOf S := by + have H₁ := h₁.2 + have H₂ := h₂.2 + constructor + · apply Set.Subset.trans h₁.1 h₂.1 + · intro x hx y hy z hz hhz + have hhhz : z ∈ F₁.carrier := Set.mem_of_mem_of_subset hz h₁.1 + have HH₂ := @H₂ x hx y hy z hhhz hhz + have hh := hhz + rw [openSegment_symm] at hh + have HHH₂ := @H₂ y hy x hx z hhhz hh + specialize @H₁ x HH₂ y HHH₂ z hz hhz + apply H₁ + +theorem iff_le_of_isFaceOf (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : +F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by + constructor + · intro h + apply h.1 + · intro hh + constructor + · apply hh + · intro x hx y hy z hz hhz + have hhx : x ∈ S.carrier := Set.mem_of_mem_of_subset hx h₂.1 + have hhy : y ∈ S.carrier := Set.mem_of_mem_of_subset hy h₂.1 + have hh₁ := h₁.2 + specialize hh₁ hhx hhy hz hhz + apply hh₁ + +theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : Convex R (S₁.carrier ∩ S₂.carrier ) := by + have hs₁ := S₁.2 + have hs₂ := S₂.2 + unfold ConvexSpace.Convex at hs₁ hs₂ + unfold ConvexSpace.Convex + intro x hx y hy a b ha hb h + have hx1 := hx.1 + have hx2 := hx.2 + have hy1 := hy.1 + have hy2 := hy.2 + specialize @hs₁ x hx1 y hy1 a b ha hb h + specialize @hs₂ x hx2 y hy2 a b ha hb h + exact Set.mem_inter hs₁ hs₂ + +def Inter (A B : ConvexSet R M) : ConvexSet R M := { + carrier := (A.carrier ∩ B.carrier), + convex := by + have h_sInter : Convex R (⋂₀ {A.carrier, B.carrier}) := by + apply ConvexSpace.convex_sInter + intro s hs + rcases hs with rfl | rfl + · exact A.convex + · exact B.convex + exact Set.sInter_pair A.carrier B.carrier ▸ h_sInter + } + +/-The intersection of two faces of two convexsets is a face of the intersection of the convexsets-/ +theorem inf (S₁ S₂ F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S₁) (h₂ : F₂.IsFaceOf S₂) : +(Inter R F₁ F₂).IsFaceOf (Inter R S₁ S₂) := by + constructor + · rw [@Set.subset_def] + intro x hx + have hhx := hx.1 + have hhhx := hx.2 + constructor + · apply Set.mem_of_mem_of_subset hhx h₁.1 + · apply Set.mem_of_mem_of_subset hhhx h₂.1 + · intro a ha b hb z hz hhz + have ha1 := ha.1 + have hb1 := hb.1 + have hz1 := hz.1 + have ha2 := ha.2 + have hb2 := hb.2 + have hz2 := hz.2 + have hh1 := h₁.2 + have hh2 := h₂.2 + specialize @hh1 a ha.1 b hb.1 z hz.1 hhz + specialize @hh2 a ha.2 b hb.2 z hz.2 hhz + constructor + · use hh1 + · use hh2 + +theorem inf_left (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : +(Inter R F₁ F₂).IsFaceOf S := by + have hh1 := h₁.1 + have hh2 := h₂.1 + constructor + · have hhh := Set.inter_subset_inter hh1 hh2 + rw[Set.inter_self] at hhh + unfold Inter + use hhh + · intro x hx y hy z hz hhz + have h1 := h₁.2 + have h2 := h₂.2 + specialize @h1 x hx y hy z hz.1 hhz + specialize @h2 x hx y hy z hz.2 hhz + use h1 + +theorem inf_right (S₁ S₂ F : ConvexSet R M) (h₁ : F.IsFaceOf S₁) (h₂ : F.IsFaceOf S₂) : +F.IsFaceOf (Inter R S₁ S₂) := by + constructor + · have hh1 := h₁.1 + have hh2 := h₂.1 + apply Set.subset_inter + · use hh1 + · use hh2 + · intro x hx y hy z hz hhz + have h1 := h₁.2 + specialize @h1 x hx.1 y hy.1 z hz hhz + use h1 + +end ConvexSet diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean new file mode 100644 index 00000000..5bdeeff5 --- /dev/null +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -0,0 +1,149 @@ +import Polyhedral.Mathlib.LinearAlgebra.ConvexSpace +import Mathlib.Analysis.Convex.Segment + + +open ConvexSpace + +namespace ConvexSet + +variable (R : Type*) {M : Type*} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] + [ConvexSpace R M] + +theorem refl (S : ConvexSet R M) : S.IsFaceOf S := by + constructor + · simp + · intro x hx y hy z hz h + apply hx + +theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by + unfold ConvexSpace.openSegment + ext z + apply Iff.intro + · intro h + simp only [Set.mem_setOf_eq] + rcases h with ⟨m, n, hm , hn , hmn , hz⟩ + use n, m, hn, hm + rw [add_comm] at hmn + use hmn + unfold convexComboPair + unfold convexCombination + sorry + · intro h + simp only [Set.mem_setOf_eq] + rcases h with ⟨m,n,hm,hn,hmn,hz⟩ + use n,m,hn,hm + rw [add_comm] at hmn + sorry + +theorem trans (S F₁ F₂ : ConvexSet R M) (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf S) : +F₂.IsFaceOf S := by + have H₁ := h₁.2 + have H₂ := h₂.2 + constructor + · apply Set.Subset.trans h₁.1 h₂.1 + · intro x hx y hy z hz hhz + have hhhz : z ∈ F₁.carrier := Set.mem_of_mem_of_subset hz h₁.1 + have HH₂ := @H₂ x hx y hy z hhhz hhz + have hh := hhz + rw [openSegment_symm] at hh + have HHH₂ := @H₂ y hy x hx z hhhz hh + specialize @H₁ x HH₂ y HHH₂ z hz hhz + apply H₁ + +theorem iff_le_of_isFaceOf (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : +F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by + constructor + · intro h + apply h.1 + · intro hh + constructor + · apply hh + · intro x hx y hy z hz hhz + have hhx : x ∈ S.carrier := Set.mem_of_mem_of_subset hx h₂.1 + have hhy : y ∈ S.carrier := Set.mem_of_mem_of_subset hy h₂.1 + have hh₁ := h₁.2 + specialize hh₁ hhx hhy hz hhz + apply hh₁ + +theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : Convex R (S₁.carrier ∩ S₂.carrier ) := by + have hs₁ := S₁.2 + have hs₂ := S₂.2 + unfold ConvexSpace.Convex at hs₁ hs₂ + unfold ConvexSpace.Convex + intro x hx y hy a b ha hb h + have hx1 := hx.1 + have hx2 := hx.2 + have hy1 := hy.1 + have hy2 := hy.2 + specialize @hs₁ x hx1 y hy1 a b ha hb h + specialize @hs₂ x hx2 y hy2 a b ha hb h + exact Set.mem_inter hs₁ hs₂ + +def Inter (A B : ConvexSet R M) : ConvexSet R M := { + carrier := (A.carrier ∩ B.carrier), + convex := by + have h_sInter : Convex R (⋂₀ {A.carrier, B.carrier}) := by + apply ConvexSpace.convex_sInter + intro s hs + rcases hs with rfl | rfl + · exact A.convex + · exact B.convex + exact Set.sInter_pair A.carrier B.carrier ▸ h_sInter + } + +/-The intersection of two faces of two convexsets is a face of the intersection of the convexsets-/ +theorem inf (S₁ S₂ F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S₁) (h₂ : F₂.IsFaceOf S₂) : +(Inter R F₁ F₂).IsFaceOf (Inter R S₁ S₂) := by + constructor + · rw [@Set.subset_def] + intro x hx + have hhx := hx.1 + have hhhx := hx.2 + constructor + · apply Set.mem_of_mem_of_subset hhx h₁.1 + · apply Set.mem_of_mem_of_subset hhhx h₂.1 + · intro a ha b hb z hz hhz + have ha1 := ha.1 + have hb1 := hb.1 + have hz1 := hz.1 + have ha2 := ha.2 + have hb2 := hb.2 + have hz2 := hz.2 + have hh1 := h₁.2 + have hh2 := h₂.2 + specialize @hh1 a ha.1 b hb.1 z hz.1 hhz + specialize @hh2 a ha.2 b hb.2 z hz.2 hhz + constructor + · use hh1 + · use hh2 + +theorem inf_left (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : +(Inter R F₁ F₂).IsFaceOf S := by + have hh1 := h₁.1 + have hh2 := h₂.1 + constructor + · have hhh := Set.inter_subset_inter hh1 hh2 + rw[Set.inter_self] at hhh + unfold Inter + use hhh + · intro x hx y hy z hz hhz + have h1 := h₁.2 + have h2 := h₂.2 + specialize @h1 x hx y hy z hz.1 hhz + specialize @h2 x hx y hy z hz.2 hhz + use h1 + +theorem inf_right (S₁ S₂ F : ConvexSet R M) (h₁ : F.IsFaceOf S₁) (h₂ : F.IsFaceOf S₂) : +F.IsFaceOf (Inter R S₁ S₂) := by + constructor + · have hh1 := h₁.1 + have hh2 := h₂.1 + apply Set.subset_inter + · use hh1 + · use hh2 + · intro x hx y hy z hz hhz + have h1 := h₁.2 + specialize @h1 x hx.1 y hy.1 z hz hhz + use h1 + +end ConvexSet From 0cb6a25dbf3d0dec0873905e43e98b931974438c Mon Sep 17 00:00:00 2001 From: VTC Date: Mon, 8 Jun 2026 12:16:25 +0200 Subject: [PATCH 02/11] ... --- .../Mathlib/LinearAlgebra/Face/Basic.lean | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean index 5bdeeff5..5e2a174b 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -1,8 +1,8 @@ -import Polyhedral.Mathlib.LinearAlgebra.ConvexSpace +import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face import Mathlib.Analysis.Convex.Segment -open ConvexSpace +open Convexity namespace ConvexSet @@ -16,7 +16,7 @@ theorem refl (S : ConvexSet R M) : S.IsFaceOf S := by apply hx theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by - unfold ConvexSpace.openSegment + unfold Convexity.openSegment ext z apply Iff.intro · intro h @@ -25,8 +25,8 @@ theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by use n, m, hn, hm rw [add_comm] at hmn use hmn - unfold convexComboPair - unfold convexCombination + unfold convexCombPair + unfold sConvexComb sorry · intro h simp only [Set.mem_setOf_eq] @@ -65,11 +65,11 @@ F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by specialize hh₁ hhx hhy hz hhz apply hh₁ -theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : Convex R (S₁.carrier ∩ S₂.carrier ) := by +theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : IsConvexSet R (S₁.carrier ∩ S₂.carrier ) := by have hs₁ := S₁.2 have hs₂ := S₂.2 - unfold ConvexSpace.Convex at hs₁ hs₂ - unfold ConvexSpace.Convex + unfold Convexity.IsConvexSet at hs₁ hs₂ + unfold Convexity.IsConvexSet intro x hx y hy a b ha hb h have hx1 := hx.1 have hx2 := hx.2 @@ -81,13 +81,13 @@ theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : Convex R (S₁.ca def Inter (A B : ConvexSet R M) : ConvexSet R M := { carrier := (A.carrier ∩ B.carrier), - convex := by - have h_sInter : Convex R (⋂₀ {A.carrier, B.carrier}) := by - apply ConvexSpace.convex_sInter + isConvexSet := by + have h_sInter : IsConvexSet R (⋂₀ {A.carrier, B.carrier}) := by + apply Convexity.IsConvexSet.sInter intro s hs rcases hs with rfl | rfl - · exact A.convex - · exact B.convex + · exact A.isConvexSet + · exact B.isConvexSet exact Set.sInter_pair A.carrier B.carrier ▸ h_sInter } From be7ea8a6d384be29cc5e199d959eef42f6385b6f Mon Sep 17 00:00:00 2001 From: VTC Date: Tue, 9 Jun 2026 13:05:20 +0200 Subject: [PATCH 03/11] fixed theorems --- .../LinearAlgebra/Face/Basic copy.lean | 149 ------------------ .../Mathlib/LinearAlgebra/Face/Basic.lean | 35 ++-- 2 files changed, 18 insertions(+), 166 deletions(-) delete mode 100644 Polyhedral/Mathlib/LinearAlgebra/Face/Basic copy.lean diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic copy.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic copy.lean deleted file mode 100644 index 5bdeeff5..00000000 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic copy.lean +++ /dev/null @@ -1,149 +0,0 @@ -import Polyhedral.Mathlib.LinearAlgebra.ConvexSpace -import Mathlib.Analysis.Convex.Segment - - -open ConvexSpace - -namespace ConvexSet - -variable (R : Type*) {M : Type*} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] - [ConvexSpace R M] - -theorem refl (S : ConvexSet R M) : S.IsFaceOf S := by - constructor - · simp - · intro x hx y hy z hz h - apply hx - -theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by - unfold ConvexSpace.openSegment - ext z - apply Iff.intro - · intro h - simp only [Set.mem_setOf_eq] - rcases h with ⟨m, n, hm , hn , hmn , hz⟩ - use n, m, hn, hm - rw [add_comm] at hmn - use hmn - unfold convexComboPair - unfold convexCombination - sorry - · intro h - simp only [Set.mem_setOf_eq] - rcases h with ⟨m,n,hm,hn,hmn,hz⟩ - use n,m,hn,hm - rw [add_comm] at hmn - sorry - -theorem trans (S F₁ F₂ : ConvexSet R M) (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf S) : -F₂.IsFaceOf S := by - have H₁ := h₁.2 - have H₂ := h₂.2 - constructor - · apply Set.Subset.trans h₁.1 h₂.1 - · intro x hx y hy z hz hhz - have hhhz : z ∈ F₁.carrier := Set.mem_of_mem_of_subset hz h₁.1 - have HH₂ := @H₂ x hx y hy z hhhz hhz - have hh := hhz - rw [openSegment_symm] at hh - have HHH₂ := @H₂ y hy x hx z hhhz hh - specialize @H₁ x HH₂ y HHH₂ z hz hhz - apply H₁ - -theorem iff_le_of_isFaceOf (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : -F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by - constructor - · intro h - apply h.1 - · intro hh - constructor - · apply hh - · intro x hx y hy z hz hhz - have hhx : x ∈ S.carrier := Set.mem_of_mem_of_subset hx h₂.1 - have hhy : y ∈ S.carrier := Set.mem_of_mem_of_subset hy h₂.1 - have hh₁ := h₁.2 - specialize hh₁ hhx hhy hz hhz - apply hh₁ - -theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : Convex R (S₁.carrier ∩ S₂.carrier ) := by - have hs₁ := S₁.2 - have hs₂ := S₂.2 - unfold ConvexSpace.Convex at hs₁ hs₂ - unfold ConvexSpace.Convex - intro x hx y hy a b ha hb h - have hx1 := hx.1 - have hx2 := hx.2 - have hy1 := hy.1 - have hy2 := hy.2 - specialize @hs₁ x hx1 y hy1 a b ha hb h - specialize @hs₂ x hx2 y hy2 a b ha hb h - exact Set.mem_inter hs₁ hs₂ - -def Inter (A B : ConvexSet R M) : ConvexSet R M := { - carrier := (A.carrier ∩ B.carrier), - convex := by - have h_sInter : Convex R (⋂₀ {A.carrier, B.carrier}) := by - apply ConvexSpace.convex_sInter - intro s hs - rcases hs with rfl | rfl - · exact A.convex - · exact B.convex - exact Set.sInter_pair A.carrier B.carrier ▸ h_sInter - } - -/-The intersection of two faces of two convexsets is a face of the intersection of the convexsets-/ -theorem inf (S₁ S₂ F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S₁) (h₂ : F₂.IsFaceOf S₂) : -(Inter R F₁ F₂).IsFaceOf (Inter R S₁ S₂) := by - constructor - · rw [@Set.subset_def] - intro x hx - have hhx := hx.1 - have hhhx := hx.2 - constructor - · apply Set.mem_of_mem_of_subset hhx h₁.1 - · apply Set.mem_of_mem_of_subset hhhx h₂.1 - · intro a ha b hb z hz hhz - have ha1 := ha.1 - have hb1 := hb.1 - have hz1 := hz.1 - have ha2 := ha.2 - have hb2 := hb.2 - have hz2 := hz.2 - have hh1 := h₁.2 - have hh2 := h₂.2 - specialize @hh1 a ha.1 b hb.1 z hz.1 hhz - specialize @hh2 a ha.2 b hb.2 z hz.2 hhz - constructor - · use hh1 - · use hh2 - -theorem inf_left (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : -(Inter R F₁ F₂).IsFaceOf S := by - have hh1 := h₁.1 - have hh2 := h₂.1 - constructor - · have hhh := Set.inter_subset_inter hh1 hh2 - rw[Set.inter_self] at hhh - unfold Inter - use hhh - · intro x hx y hy z hz hhz - have h1 := h₁.2 - have h2 := h₂.2 - specialize @h1 x hx y hy z hz.1 hhz - specialize @h2 x hx y hy z hz.2 hhz - use h1 - -theorem inf_right (S₁ S₂ F : ConvexSet R M) (h₁ : F.IsFaceOf S₁) (h₂ : F.IsFaceOf S₂) : -F.IsFaceOf (Inter R S₁ S₂) := by - constructor - · have hh1 := h₁.1 - have hh2 := h₂.1 - apply Set.subset_inter - · use hh1 - · use hh2 - · intro x hx y hy z hz hhz - have h1 := h₁.2 - specialize @h1 x hx.1 y hy.1 z hz hhz - use h1 - -end ConvexSet diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean index 5e2a174b..8aded8b7 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -1,4 +1,4 @@ -import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face +import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Basic import Mathlib.Analysis.Convex.Segment @@ -20,20 +20,17 @@ theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by ext z apply Iff.intro · intro h - simp only [Set.mem_setOf_eq] rcases h with ⟨m, n, hm , hn , hmn , hz⟩ use n, m, hn, hm + rw [convexCombPair_symm] at hz rw [add_comm] at hmn use hmn - unfold convexCombPair - unfold sConvexComb - sorry · intro h - simp only [Set.mem_setOf_eq] - rcases h with ⟨m,n,hm,hn,hmn,hz⟩ - use n,m,hn,hm + rcases h with ⟨m, n, hm , hn , hmn , hz⟩ + use n, m, hn, hm + rw [convexCombPair_symm] at hz rw [add_comm] at hmn - sorry + use hmn theorem trans (S F₁ F₂ : ConvexSet R M) (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf S) : F₂.IsFaceOf S := by @@ -70,14 +67,13 @@ theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : IsConvexSet R (S have hs₂ := S₂.2 unfold Convexity.IsConvexSet at hs₁ hs₂ unfold Convexity.IsConvexSet - intro x hx y hy a b ha hb h - have hx1 := hx.1 - have hx2 := hx.2 - have hy1 := hy.1 - have hy2 := hy.2 - specialize @hs₁ x hx1 y hy1 a b ha hb h - specialize @hs₂ x hx2 y hy2 a b ha hb h - exact Set.mem_inter hs₁ hs₂ + intro w hw + simp at hw + constructor + · specialize @hs₁ w hw.1 + apply hs₁ + · specialize @hs₂ w hw.2 + apply hs₂ def Inter (A B : ConvexSet R M) : ConvexSet R M := { carrier := (A.carrier ∩ B.carrier), @@ -132,6 +128,7 @@ theorem inf_left (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : specialize @h1 x hx y hy z hz.1 hhz specialize @h2 x hx y hy z hz.2 hhz use h1 + use h2 theorem inf_right (S₁ S₂ F : ConvexSet R M) (h₁ : F.IsFaceOf S₁) (h₂ : F.IsFaceOf S₂) : F.IsFaceOf (Inter R S₁ S₂) := by @@ -146,4 +143,8 @@ F.IsFaceOf (Inter R S₁ S₂) := by specialize @h1 x hx.1 y hy.1 z hz hhz use h1 +#check AffineMap + + + end ConvexSet From 5ec53035990bce507e7a0ca0adfe69833df8811e Mon Sep 17 00:00:00 2001 From: Mara Gruss Date: Tue, 9 Jun 2026 14:55:11 +0200 Subject: [PATCH 04/11] fixed theorems --- .../Mathlib/LinearAlgebra/Face/Basic.lean | 46 +++++++++++-------- 1 file changed, 28 insertions(+), 18 deletions(-) diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean index 5e2a174b..66880f00 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -1,13 +1,20 @@ -import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face +import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Basic import Mathlib.Analysis.Convex.Segment - +import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.AffineSpace open Convexity - -namespace ConvexSet +open Affine Convexity variable (R : Type*) {M : Type*} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [ConvexSpace R M] +variable {K V V2 P P2 I N L : Type*} +variable [Ring K] [PartialOrder K] [IsStrictOrderedRing K] +variable [AddCommGroup N] [Module K N] [ConvexSpace K N] +variable [AddCommGroup L] [Module K L] +variable [AddCommGroup V] [Module K V] [AddTorsor V P] +variable [AddCommGroup V2] [Module K V2] [AffineSpace V2 P2] + +namespace ConvexSet theorem refl (S : ConvexSet R M) : S.IsFaceOf S := by constructor @@ -20,20 +27,17 @@ theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by ext z apply Iff.intro · intro h - simp only [Set.mem_setOf_eq] rcases h with ⟨m, n, hm , hn , hmn , hz⟩ use n, m, hn, hm + rw [convexCombPair_symm] at hz rw [add_comm] at hmn use hmn - unfold convexCombPair - unfold sConvexComb - sorry · intro h - simp only [Set.mem_setOf_eq] rcases h with ⟨m,n,hm,hn,hmn,hz⟩ use n,m,hn,hm + rw [convexCombPair_symm] at hz rw [add_comm] at hmn - sorry + use hmn theorem trans (S F₁ F₂ : ConvexSet R M) (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf S) : F₂.IsFaceOf S := by @@ -70,14 +74,11 @@ theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : IsConvexSet R (S have hs₂ := S₂.2 unfold Convexity.IsConvexSet at hs₁ hs₂ unfold Convexity.IsConvexSet - intro x hx y hy a b ha hb h - have hx1 := hx.1 - have hx2 := hx.2 - have hy1 := hy.1 - have hy2 := hy.2 - specialize @hs₁ x hx1 y hy1 a b ha hb h - specialize @hs₂ x hx2 y hy2 a b ha hb h - exact Set.mem_inter hs₁ hs₂ + intro w hw + simp at hw + specialize @hs₁ w hw.1 + specialize @hs₂ w hw.2 + use hs₁ def Inter (A B : ConvexSet R M) : ConvexSet R M := { carrier := (A.carrier ∩ B.carrier), @@ -117,6 +118,7 @@ theorem inf (S₁ S₂ F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S₁) (h · use hh1 · use hh2 +/- The intersection of two faces is a face.-/ theorem inf_left (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : (Inter R F₁ F₂).IsFaceOf S := by have hh1 := h₁.1 @@ -132,7 +134,9 @@ theorem inf_left (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : specialize @h1 x hx y hy z hz.1 hhz specialize @h2 x hx y hy z hz.2 hhz use h1 + use h2 +/- The face of two convexsets is a face of the intersection.-/ theorem inf_right (S₁ S₂ F : ConvexSet R M) (h₁ : F.IsFaceOf S₁) (h₂ : F.IsFaceOf S₂) : F.IsFaceOf (Inter R S₁ S₂) := by constructor @@ -146,4 +150,10 @@ F.IsFaceOf (Inter R S₁ S₂) := by specialize @h1 x hx.1 y hy.1 z hz hhz use h1 +theorem convexmap (f : N →ᵃ[K] L) (C : ConvexSet K N) : (C.map f).isConvexSet := by + sorry + +theorem map (f : N →ᵃ[K] L) (hf : Function.Injective f) (F C : ConvexSet K N) (hF : F.IsFaceOf C) : + (F.map f).IsFaceOf (C.map f) := by + sorry end ConvexSet From a78b4adcaf5c3cd74310fe9e8d13201772159671 Mon Sep 17 00:00:00 2001 From: Mara Gruss Date: Tue, 9 Jun 2026 17:35:30 +0200 Subject: [PATCH 05/11] proved faces under affine map --- .../Mathlib/LinearAlgebra/Face/Basic.lean | 41 +++++++++++++------ 1 file changed, 28 insertions(+), 13 deletions(-) diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean index 66880f00..2132f08a 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -5,14 +5,8 @@ import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.AffineSpace open Convexity open Affine Convexity -variable (R : Type*) {M : Type*} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] - [ConvexSpace R M] -variable {K V V2 P P2 I N L : Type*} -variable [Ring K] [PartialOrder K] [IsStrictOrderedRing K] -variable [AddCommGroup N] [Module K N] [ConvexSpace K N] -variable [AddCommGroup L] [Module K L] -variable [AddCommGroup V] [Module K V] [AddTorsor V P] -variable [AddCommGroup V2] [Module K V2] [AffineSpace V2 P2] +variable (R : Type*) {M N : Type*} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] + [ConvexSpace R M] [ConvexSpace R N] namespace ConvexSet @@ -150,10 +144,31 @@ F.IsFaceOf (Inter R S₁ S₂) := by specialize @h1 x hx.1 y hy.1 z hz hhz use h1 -theorem convexmap (f : N →ᵃ[K] L) (C : ConvexSet K N) : (C.map f).isConvexSet := by - sorry +theorem map {f : M -> N} (hhf : IsAffineMap R f) (hf : Function.Injective f) (F C : ConvexSet R M) + (hF : F.IsFaceOf C) : + (F.map hhf).IsFaceOf (C.map hhf) := by + constructor + · have hF1 := hF.1 + intro x hx + rcases hx with ⟨y , hy, rfl⟩ + have hy1 : y ∈ C.carrier := Set.mem_of_mem_of_subset hy hF1 + apply Set.mem_image_of_mem + use hy1 + · intro x hx y hy z hz hhz + rcases hx with ⟨m , hmC, rfl⟩ + rcases hy with ⟨n , hnC, rfl⟩ + rcases hz with ⟨l , hlF, rfl⟩ + have hl : l ∈ Convexity.openSegment R m n := by + rcases hhz with ⟨ a, b, ha, hb, hab, hcomb⟩ + have hfcomb := (hhf.map_sConvexComb) + have h : f (convexCombPair a b ha.le hb.le hab m n) = + convexCombPair a b ha.le hb.le hab (f m) (f n) := hhf.map_convexCombPair ha.le hb.le hab m n + have hh : f (convexCombPair a b ha.le hb.le hab m n) = f l := by + simpa [h] using hcomb + exact ⟨ a, b, ha, hb, hab, hf hh⟩ + have hF2 := hF.2 + specialize @hF2 m hmC n hnC l hlF hl + apply Set.mem_image_of_mem + use hF2 -theorem map (f : N →ᵃ[K] L) (hf : Function.Injective f) (F C : ConvexSet K N) (hF : F.IsFaceOf C) : - (F.map f).IsFaceOf (C.map f) := by - sorry end ConvexSet From c3c99c89769550897ac2336ee8f45aa57974ba6b Mon Sep 17 00:00:00 2001 From: VTC Date: Tue, 9 Jun 2026 15:56:27 +0200 Subject: [PATCH 06/11] thm inter convexset --- Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean index be8cb870..1fa4cb68 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -63,13 +63,14 @@ F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by specialize hh₁ hhx hhy hz hhz apply hh₁ -theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : IsConvexSet R (S₁.carrier ∩ S₂.carrier ) := by +theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : IsConvexSet R (S₁.carrier ∩ S₂.carrier ) +:= by have hs₁ := S₁.2 have hs₂ := S₂.2 unfold Convexity.IsConvexSet at hs₁ hs₂ unfold Convexity.IsConvexSet intro w hw - simp at hw + rw [Set.subset_inter_iff] at hw specialize @hs₁ w hw.1 specialize @hs₂ w hw.2 use hs₁ From 54bb3dea37608d822f5387bcfa768e72e503f6fa Mon Sep 17 00:00:00 2001 From: VTC Date: Tue, 16 Jun 2026 14:44:32 +0200 Subject: [PATCH 07/11] thms faces convexsets affine maps --- .../Mathlib/LinearAlgebra/Face/Basic.lean | 45 ++++++++++++++++++- 1 file changed, 44 insertions(+), 1 deletion(-) diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean index 1fa4cb68..682f5db1 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -63,6 +63,23 @@ F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by specialize hh₁ hhx hhy hz hhz apply hh₁ +lemma isFaceOf_iff (F C F₁ : ConvexSet R M) (H : F.IsFaceOf C) : +F₁.IsFaceOf F ↔ F₁.carrier ⊆ F.carrier ∧ F₁.IsFaceOf C:= by + apply Iff.intro + · intro h + constructor + · apply h.1 + · apply trans R C F F₁ h H + · intro h + constructor + · apply h.1 + · have h₁ := h.2.2 + intro x hx y hy z hz hhz + have hhx : x ∈ C.carrier := Set.mem_of_mem_of_subset hx H.1 + have hhy : y ∈ C.carrier := Set.mem_of_mem_of_subset hy H.1 + specialize @h₁ x hhx y hhy z hz hhz + use h₁ + theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : IsConvexSet R (S₁.carrier ∩ S₂.carrier ) := by have hs₁ := S₁.2 @@ -70,7 +87,7 @@ theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : IsConvexSet R (S unfold Convexity.IsConvexSet at hs₁ hs₂ unfold Convexity.IsConvexSet intro w hw - rw [Set.subset_inter_iff] at hw + rw [Set.subset_inter_iff] at hw specialize @hs₁ w hw.1 specialize @hs₂ w hw.2 use hs₁ @@ -172,4 +189,30 @@ theorem map {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective f) (F apply Set.mem_image_of_mem use hF2 +theorem isFaceOf_map_iff (f : M → N) (hhf : IsAffineMap R f) (hf : Function.Injective f) +(C F : ConvexSet R M):(F.map hhf).IsFaceOf (C.map hhf) ↔ F.IsFaceOf C := by + apply Iff.intro + · intro h + constructor + · have h₁ := h.1 + have h' := (Set.image_subset_image_iff hf).mp h₁ + use h' + · intro x hx y hy z hz hhz + have hx' : f x ∈ (C.map hhf) := Set.mem_image_of_mem f hx + have hy' : f y ∈ (C.map hhf) := Set.mem_image_of_mem f hy + have hz' : f z ∈ (F.map hhf) := Set.mem_image_of_mem f hz + have hhz' : f z ∈ Convexity.openSegment R (f x) (f y) := by + rcases hhz with ⟨ a, b, ha, hb, hab, hcomb⟩ + have hff : f (convexCombPair a b ha.le hb.le hab x y) = + convexCombPair a b ha.le hb.le hab (f x) (f y) := hhf.map_convexCombPair ha.le hb.le hab x y + rw [hcomb] at hff + unfold Convexity.openSegment + use a, b, ha, hb, hab + use hff.symm + have h2 := h.2 + specialize @h2 (f x) hx' (f y) hy' (f z) hz' hhz' + exact (Function.Injective.mem_set_image hf).mp h2 + · intro h + apply map R hhf hf F C h + end ConvexSet From 328bba35178d0395ef45eb7cd046e70a98b161de Mon Sep 17 00:00:00 2001 From: Mara Gruss Date: Tue, 16 Jun 2026 16:46:42 +0200 Subject: [PATCH 08/11] some short proof versions --- .../Mathlib/LinearAlgebra/Face/Basic.lean | 94 +++++++++++++++++-- 1 file changed, 87 insertions(+), 7 deletions(-) diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean index 682f5db1..8eabb5cb 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -16,6 +16,9 @@ theorem refl (S : ConvexSet R M) : S.IsFaceOf S := by · intro x hx y hy z hz h apply hx +theorem refl_short (S : ConvexSet R M) : S.IsFaceOf S := + ⟨by simp , by intro x hx y hy z hz h; apply hx⟩ + theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by unfold Convexity.openSegment ext z @@ -33,6 +36,13 @@ theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by rw [add_comm] at hmn use hmn +theorem openSegment_symm_short (x y : M) : openSegment R x y = openSegment R y x := by + unfold Convexity.openSegment + ext z + constructor + all_goals (intro h; rcases h with ⟨m, n, hm , hn , hmn , hz⟩; use n, m, hn, hm) + all_goals (rw [convexCombPair_symm] at hz; rw [add_comm] at hmn; use hmn) + theorem trans (S F₁ F₂ : ConvexSet R M) (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf S) : F₂.IsFaceOf S := by have H₁ := h₁.2 @@ -48,6 +58,17 @@ F₂.IsFaceOf S := by specialize @H₁ x HH₂ y HHH₂ z hz hhz apply H₁ +theorem trans_short (S F₁ F₂ : ConvexSet R M) (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf S) : +F₂.IsFaceOf S := by + constructor + · apply Set.Subset.trans h₁.1 h₂.1 + · intro x hx y hy z hz hhz + have hz' : z ∈ F₁.carrier := Set.mem_of_mem_of_subset hz h₁.1 + have H := @h₂.2 x hx y hy z hz' hhz + have HH := @h₂.2 y hy x hx z hz' (by simpa [openSegment_symm] using hhz) + have HHH := @h₁.2 x H y HH z hz hhz + apply HHH + theorem iff_le_of_isFaceOf (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by constructor @@ -63,6 +84,19 @@ F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by specialize hh₁ hhx hhy hz hhz apply hh₁ +theorem iff_le_of_isFaceOf_short (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) + (h₂ : F₂.IsFaceOf S) : +F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by + constructor + · exact fun h => h.1 + · intro hh + constructor + · exact hh + · intro x hx y hy z hz hhz + have hhx : x ∈ S.carrier := Set.mem_of_mem_of_subset hx h₂.1 + have hhy : y ∈ S.carrier := Set.mem_of_mem_of_subset hy h₂.1 + exact h₁.2 hhx hhy hz hhz + lemma isFaceOf_iff (F C F₁ : ConvexSet R M) (H : F.IsFaceOf C) : F₁.IsFaceOf F ↔ F₁.carrier ⊆ F.carrier ∧ F₁.IsFaceOf C:= by apply Iff.intro @@ -80,6 +114,19 @@ F₁.IsFaceOf F ↔ F₁.carrier ⊆ F.carrier ∧ F₁.IsFaceOf C:= by specialize @h₁ x hhx y hhy z hz hhz use h₁ +lemma isFaceOf_iff_short (F C F₁ : ConvexSet R M) (H : F.IsFaceOf C) : +F₁.IsFaceOf F ↔ F₁.carrier ⊆ F.carrier ∧ F₁.IsFaceOf C:= by + apply Iff.intro + · exact fun h => ⟨h.1, trans R C F F₁ h H⟩ + · intro h + constructor + · apply h.1 + · intro x hx y hy z hz hhz + have hhx : x ∈ C.carrier := Set.mem_of_mem_of_subset hx H.1 + have hhy : y ∈ C.carrier := Set.mem_of_mem_of_subset hy H.1 + have h1 := @h.2.2 x hhx y hhy z hz hhz + use h1 + theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : IsConvexSet R (S₁.carrier ∩ S₂.carrier ) := by have hs₁ := S₁.2 @@ -116,12 +163,6 @@ theorem inf (S₁ S₂ F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S₁) (h · apply Set.mem_of_mem_of_subset hhx h₁.1 · apply Set.mem_of_mem_of_subset hhhx h₂.1 · intro a ha b hb z hz hhz - have ha1 := ha.1 - have hb1 := hb.1 - have hz1 := hz.1 - have ha2 := ha.2 - have hb2 := hb.2 - have hz2 := hz.2 have hh1 := h₁.2 have hh2 := h₂.2 specialize @hh1 a ha.1 b hb.1 z hz.1 hhz @@ -130,6 +171,16 @@ theorem inf (S₁ S₂ F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S₁) (h · use hh1 · use hh2 +theorem inf_short (S₁ S₂ F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S₁) (h₂ : F₂.IsFaceOf S₂) : +(Inter R F₁ F₂).IsFaceOf (Inter R S₁ S₂) := by + constructor + · rw [@Set.subset_def] + exact fun x hx => ⟨Set.mem_of_mem_of_subset hx.1 h₁.1, Set.mem_of_mem_of_subset hx.2 h₂.1⟩ + · intro a ha b hb z hz hhz + have hh1 := @h₁.2 a ha.1 b hb.1 z hz.1 hhz + have hh2 := @h₂.2 a ha.2 b hb.2 z hz.2 hhz + exact ⟨hh1, hh2⟩ + /- The intersection of two faces is a face.-/ theorem inf_left (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : (Inter R F₁ F₂).IsFaceOf S := by @@ -148,6 +199,13 @@ theorem inf_left (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : use h1 use h2 +theorem inf_left_short (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : +(Inter R F₁ F₂).IsFaceOf S := by + constructor + · simpa [Set.inter_self] using Set.inter_subset_inter h₁.1 h₂.1 + · intro x hx y hy z hz hhz + exact ⟨@h₁.2 x hx y hy z hz.1 hhz, @h₂.2 x hx y hy z hz.2 hhz⟩ + /- The face of two convexsets is a face of the intersection.-/ theorem inf_right (S₁ S₂ F : ConvexSet R M) (h₁ : F.IsFaceOf S₁) (h₂ : F.IsFaceOf S₂) : F.IsFaceOf (Inter R S₁ S₂) := by @@ -162,6 +220,10 @@ F.IsFaceOf (Inter R S₁ S₂) := by specialize @h1 x hx.1 y hy.1 z hz hhz use h1 +theorem inf_right_short (S₁ S₂ F : ConvexSet R M) (h₁ : F.IsFaceOf S₁) (h₂ : F.IsFaceOf S₂) : +F.IsFaceOf (Inter R S₁ S₂) := + ⟨Set.subset_inter h₁.1 h₂.1, by intro x hx y hy z hz hhz; exact @h₁.2 x hx.1 y hy.1 z hz hhz⟩ + theorem map {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective f) (F C : ConvexSet R M) (hF : F.IsFaceOf C) : (F.map hhf).IsFaceOf (C.map hhf) := by @@ -178,7 +240,6 @@ theorem map {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective f) (F rcases hz with ⟨l , hlF, rfl⟩ have hl : l ∈ Convexity.openSegment R m n := by rcases hhz with ⟨ a, b, ha, hb, hab, hcomb⟩ - have hfcomb := (hhf.map_sConvexComb) have h : f (convexCombPair a b ha.le hb.le hab m n) = convexCombPair a b ha.le hb.le hab (f m) (f n) := hhf.map_convexCombPair ha.le hb.le hab m n have hh : f (convexCombPair a b ha.le hb.le hab m n) = f l := by @@ -189,6 +250,25 @@ theorem map {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective f) (F apply Set.mem_image_of_mem use hF2 +theorem map_short {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective f) + (F C : ConvexSet R M) (hF : F.IsFaceOf C) : (F.map hhf).IsFaceOf (C.map hhf) := by + constructor + · intro x hx + rcases hx with ⟨y , hy, rfl⟩ + exact Set.mem_image_of_mem _ (Set.mem_of_mem_of_subset hy hF.1) + · intro x hx y hy z hz hhz + rcases hx with ⟨m , hmC, rfl⟩ + rcases hy with ⟨n , hnC, rfl⟩ + rcases hz with ⟨l , hlF, rfl⟩ + have hl : l ∈ Convexity.openSegment R m n := by + rcases hhz with ⟨ a, b, ha, hb, hab, hcomb⟩ + have h : f (convexCombPair a b ha.le hb.le hab m n) = + convexCombPair a b ha.le hb.le hab (f m) (f n) := hhf.map_convexCombPair ha.le hb.le hab m n + have hh : f (convexCombPair a b ha.le hb.le hab m n) = f l := by + simpa [h] using hcomb + exact ⟨ a, b, ha, hb, hab, hf hh⟩ + exact Set.mem_image_of_mem _ (@hF.2 m hmC n hnC l hlF hl) + theorem isFaceOf_map_iff (f : M → N) (hhf : IsAffineMap R f) (hf : Function.Injective f) (C F : ConvexSet R M):(F.map hhf).IsFaceOf (C.map hhf) ↔ F.IsFaceOf C := by apply Iff.intro From 73206a86eb9b18be978e14b6207fab96c4fb904a Mon Sep 17 00:00:00 2001 From: VTC Date: Tue, 16 Jun 2026 16:50:27 +0200 Subject: [PATCH 09/11] comap def --- .../Mathlib/LinearAlgebra/Face/Basic.lean | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean index 682f5db1..39e1644b 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -63,6 +63,8 @@ F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by specialize hh₁ hhx hhy hz hhz apply hh₁ +/-A convex set is a face of a face iff it is contained in the face and it is a face +of the ambient set-/ lemma isFaceOf_iff (F C F₁ : ConvexSet R M) (H : F.IsFaceOf C) : F₁.IsFaceOf F ↔ F₁.carrier ⊆ F.carrier ∧ F₁.IsFaceOf C:= by apply Iff.intro @@ -80,6 +82,7 @@ F₁.IsFaceOf F ↔ F₁.carrier ⊆ F.carrier ∧ F₁.IsFaceOf C:= by specialize @h₁ x hhx y hhy z hz hhz use h₁ +/-intersection of two convex sets is a convex set -/ theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : IsConvexSet R (S₁.carrier ∩ S₂.carrier ) := by have hs₁ := S₁.2 @@ -162,6 +165,7 @@ F.IsFaceOf (Inter R S₁ S₂) := by specialize @h1 x hx.1 y hy.1 z hz hhz use h1 +/- The image of a face under an injective affine map is a face. -/ theorem map {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective f) (F C : ConvexSet R M) (hF : F.IsFaceOf C) : (F.map hhf).IsFaceOf (C.map hhf) := by @@ -189,6 +193,7 @@ theorem map {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective f) (F apply Set.mem_image_of_mem use hF2 +/- F is a face of C iff the image of F is a face of the image of C under and injective affine map -/ theorem isFaceOf_map_iff (f : M → N) (hhf : IsAffineMap R f) (hf : Function.Injective f) (C F : ConvexSet R M):(F.map hhf).IsFaceOf (C.map hhf) ↔ F.IsFaceOf C := by apply Iff.intro @@ -215,4 +220,23 @@ theorem isFaceOf_map_iff (f : M → N) (hhf : IsAffineMap R f) (hf : Function.In · intro h apply map R hhf hf F C h +def comap {f : M → N} (hf : IsAffineMap R f) (C : ConvexSet R N) : ConvexSet R M := { + carrier := f ⁻¹' C.carrier, + isConvexSet := by apply Convexity.IsConvexSet.preimage hf C.isConvexSet +} + +theorem of_comap_surjective {f : M → N} (hf : IsAffineMap R f) (hhf : Function.Surjective f) (F C : ConvexSet R N) +(hF : (F.comap hf).IsFaceOf (C.comap hf)) : F.IsFaceOf C := by + constructor + · have hF1 := hF.1 + have h1 : f '' (F.comap hf).carrier = F.carrier := by + apply Set.image_preimage_eq F hhf + have h2 : f '' (C.comap hf).carrier = C.carrier := by + apply Set.image_preimage_eq C hhf + have hF1' : f '' (F.comap hf).carrier ⊆ f '' (C.comap hf).carrier := by + sorry + · have hF1 := hF.2 + + sorry + end ConvexSet From 5f1949f93d3184923e4e77028c3a9e3a2949509e Mon Sep 17 00:00:00 2001 From: VTC Date: Tue, 30 Jun 2026 06:02:04 +0200 Subject: [PATCH 10/11] short version --- .../Mathlib/LinearAlgebra/Face/Basic.lean | 278 ++++-------------- 1 file changed, 55 insertions(+), 223 deletions(-) diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean index bf586ce4..f55254e9 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -10,85 +10,30 @@ variable (R : Type*) {M N : Type*} [PartialOrder R] [Semiring R] [IsStrictOrdere namespace ConvexSet -theorem refl (S : ConvexSet R M) : S.IsFaceOf S := by - constructor - · simp - · intro x hx y hy z hz h - apply hx - -theorem refl_short (S : ConvexSet R M) : S.IsFaceOf S := +/- S is a face of itself -/ +theorem refl (S : ConvexSet R M) : S.IsFaceOf S := ⟨by simp , by intro x hx y hy z hz h; apply hx⟩ +/- (x,y)=(y,x) -/ theorem openSegment_symm (x y : M) : openSegment R x y = openSegment R y x := by - unfold Convexity.openSegment - ext z - apply Iff.intro - · intro h - rcases h with ⟨m, n, hm , hn , hmn , hz⟩ - use n, m, hn, hm - rw [convexCombPair_symm] at hz - rw [add_comm] at hmn - use hmn - · intro h - rcases h with ⟨m, n, hm , hn , hmn , hz⟩ - use n, m, hn, hm - rw [convexCombPair_symm] at hz - rw [add_comm] at hmn - use hmn - -theorem openSegment_symm_short (x y : M) : openSegment R x y = openSegment R y x := by unfold Convexity.openSegment ext z constructor all_goals (intro h; rcases h with ⟨m, n, hm , hn , hmn , hz⟩; use n, m, hn, hm) all_goals (rw [convexCombPair_symm] at hz; rw [add_comm] at hmn; use hmn) +/- transitivity of faces -/ theorem trans (S F₁ F₂ : ConvexSet R M) (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf S) : -F₂.IsFaceOf S := by - have H₁ := h₁.2 - have H₂ := h₂.2 - constructor - · apply Set.Subset.trans h₁.1 h₂.1 - · intro x hx y hy z hz hhz - have hhhz : z ∈ F₁.carrier := Set.mem_of_mem_of_subset hz h₁.1 - have HH₂ := @H₂ x hx y hy z hhhz hhz - have hh := hhz - rw [openSegment_symm] at hh - have HHH₂ := @H₂ y hy x hx z hhhz hh - specialize @H₁ x HH₂ y HHH₂ z hz hhz - apply H₁ - -theorem trans_short (S F₁ F₂ : ConvexSet R M) (h₁ : F₂.IsFaceOf F₁) (h₂ : F₁.IsFaceOf S) : F₂.IsFaceOf S := by constructor · apply Set.Subset.trans h₁.1 h₂.1 · intro x hx y hy z hz hhz have hz' : z ∈ F₁.carrier := Set.mem_of_mem_of_subset hz h₁.1 - have H := @h₂.2 x hx y hy z hz' hhz - have HH := @h₂.2 y hy x hx z hz' (by simpa [openSegment_symm] using hhz) - have HHH := @h₁.2 x H y HH z hz hhz - apply HHH - -theorem iff_le_of_isFaceOf (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : -F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by - constructor - · intro h - apply h.1 - · intro hh - constructor - · apply hh - · intro x hx y hy z hz hhz - have hhx : x ∈ S.carrier := Set.mem_of_mem_of_subset hx h₂.1 - have hhy : y ∈ S.carrier := Set.mem_of_mem_of_subset hy h₂.1 - have hh₁ := h₁.2 - specialize hh₁ hhx hhy hz hhz - apply hh₁ + exact @h₁.2 x (@h₂.2 x hx y hy z hz' hhz) y (@h₂.2 y hy x hx z hz' (by simpa [openSegment_symm] + using hhz)) z hz hhz -<<<<<<< HEAD -/-A convex set is a face of a face iff it is contained in the face and it is a face -of the ambient set-/ -======= -theorem iff_le_of_isFaceOf_short (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) +/- smaller faces are faces of bigger faces -/ +theorem iff_le_of_isFaceOf (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by constructor @@ -97,32 +42,11 @@ F₁.IsFaceOf F₂ ↔ F₁.carrier ⊆ F₂.carrier := by constructor · exact hh · intro x hx y hy z hz hhz - have hhx : x ∈ S.carrier := Set.mem_of_mem_of_subset hx h₂.1 - have hhy : y ∈ S.carrier := Set.mem_of_mem_of_subset hy h₂.1 - exact h₁.2 hhx hhy hz hhz + exact h₁.2 (Set.mem_of_mem_of_subset hx h₂.1) (Set.mem_of_mem_of_subset hy h₂.1) hz hhz ->>>>>>> 328bba35178d0395ef45eb7cd046e70a98b161de +/-A convex set is a face of a face iff it is contained in the face and it is a face +of the ambient set-/ lemma isFaceOf_iff (F C F₁ : ConvexSet R M) (H : F.IsFaceOf C) : -F₁.IsFaceOf F ↔ F₁.carrier ⊆ F.carrier ∧ F₁.IsFaceOf C:= by - apply Iff.intro - · intro h - constructor - · apply h.1 - · apply trans R C F F₁ h H - · intro h - constructor - · apply h.1 - · have h₁ := h.2.2 - intro x hx y hy z hz hhz - have hhx : x ∈ C.carrier := Set.mem_of_mem_of_subset hx H.1 - have hhy : y ∈ C.carrier := Set.mem_of_mem_of_subset hy H.1 - specialize @h₁ x hhx y hhy z hz hhz - use h₁ - -<<<<<<< HEAD -/-intersection of two convex sets is a convex set -/ -======= -lemma isFaceOf_iff_short (F C F₁ : ConvexSet R M) (H : F.IsFaceOf C) : F₁.IsFaceOf F ↔ F₁.carrier ⊆ F.carrier ∧ F₁.IsFaceOf C:= by apply Iff.intro · exact fun h => ⟨h.1, trans R C F F₁ h H⟩ @@ -130,24 +54,16 @@ F₁.IsFaceOf F ↔ F₁.carrier ⊆ F.carrier ∧ F₁.IsFaceOf C:= by constructor · apply h.1 · intro x hx y hy z hz hhz - have hhx : x ∈ C.carrier := Set.mem_of_mem_of_subset hx H.1 - have hhy : y ∈ C.carrier := Set.mem_of_mem_of_subset hy H.1 - have h1 := @h.2.2 x hhx y hhy z hz hhz - use h1 + exact @h.2.2 x (Set.mem_of_mem_of_subset hx H.1) y (Set.mem_of_mem_of_subset hy H.1) z hz hhz ->>>>>>> 328bba35178d0395ef45eb7cd046e70a98b161de +/-intersection of two convex sets is a convex set -/ theorem intersection_convexsets (S₁ S₂ : ConvexSet R M) : IsConvexSet R (S₁.carrier ∩ S₂.carrier ) := by - have hs₁ := S₁.2 - have hs₂ := S₂.2 - unfold Convexity.IsConvexSet at hs₁ hs₂ - unfold Convexity.IsConvexSet intro w hw rw [Set.subset_inter_iff] at hw - specialize @hs₁ w hw.1 - specialize @hs₂ w hw.2 - use hs₁ + exact ⟨@S₁.2 w hw.1, @S₂.2 w hw.2⟩ +/- definition of intersection of convex sets -/ def Inter (A B : ConvexSet R M) : ConvexSet R M := { carrier := (A.carrier ∩ B.carrier), isConvexSet := by @@ -162,53 +78,15 @@ def Inter (A B : ConvexSet R M) : ConvexSet R M := { /-The intersection of two faces of two convexsets is a face of the intersection of the convexsets-/ theorem inf (S₁ S₂ F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S₁) (h₂ : F₂.IsFaceOf S₂) : -(Inter R F₁ F₂).IsFaceOf (Inter R S₁ S₂) := by - constructor - · rw [@Set.subset_def] - intro x hx - have hhx := hx.1 - have hhhx := hx.2 - constructor - · apply Set.mem_of_mem_of_subset hhx h₁.1 - · apply Set.mem_of_mem_of_subset hhhx h₂.1 - · intro a ha b hb z hz hhz - have hh1 := h₁.2 - have hh2 := h₂.2 - specialize @hh1 a ha.1 b hb.1 z hz.1 hhz - specialize @hh2 a ha.2 b hb.2 z hz.2 hhz - constructor - · use hh1 - · use hh2 - -theorem inf_short (S₁ S₂ F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S₁) (h₂ : F₂.IsFaceOf S₂) : (Inter R F₁ F₂).IsFaceOf (Inter R S₁ S₂) := by constructor · rw [@Set.subset_def] exact fun x hx => ⟨Set.mem_of_mem_of_subset hx.1 h₁.1, Set.mem_of_mem_of_subset hx.2 h₂.1⟩ · intro a ha b hb z hz hhz - have hh1 := @h₁.2 a ha.1 b hb.1 z hz.1 hhz - have hh2 := @h₂.2 a ha.2 b hb.2 z hz.2 hhz - exact ⟨hh1, hh2⟩ + exact ⟨@h₁.2 a ha.1 b hb.1 z hz.1 hhz, @h₂.2 a ha.2 b hb.2 z hz.2 hhz⟩ /- The intersection of two faces is a face.-/ theorem inf_left (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : -(Inter R F₁ F₂).IsFaceOf S := by - have hh1 := h₁.1 - have hh2 := h₂.1 - constructor - · have hhh := Set.inter_subset_inter hh1 hh2 - rw[Set.inter_self] at hhh - unfold Inter - use hhh - · intro x hx y hy z hz hhz - have h1 := h₁.2 - have h2 := h₂.2 - specialize @h1 x hx y hy z hz.1 hhz - specialize @h2 x hx y hy z hz.2 hhz - use h1 - use h2 - -theorem inf_left_short (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h₂ : F₂.IsFaceOf S) : (Inter R F₁ F₂).IsFaceOf S := by constructor · simpa [Set.inter_self] using Set.inter_subset_inter h₁.1 h₂.1 @@ -217,56 +95,11 @@ theorem inf_left_short (S F₁ F₂ : ConvexSet R M) (h₁ : F₁.IsFaceOf S) (h /- The face of two convexsets is a face of the intersection.-/ theorem inf_right (S₁ S₂ F : ConvexSet R M) (h₁ : F.IsFaceOf S₁) (h₂ : F.IsFaceOf S₂) : -F.IsFaceOf (Inter R S₁ S₂) := by - constructor - · have hh1 := h₁.1 - have hh2 := h₂.1 - apply Set.subset_inter - · use hh1 - · use hh2 - · intro x hx y hy z hz hhz - have h1 := h₁.2 - specialize @h1 x hx.1 y hy.1 z hz hhz - use h1 - -<<<<<<< HEAD -/- The image of a face under an injective affine map is a face. -/ -======= -theorem inf_right_short (S₁ S₂ F : ConvexSet R M) (h₁ : F.IsFaceOf S₁) (h₂ : F.IsFaceOf S₂) : F.IsFaceOf (Inter R S₁ S₂) := ⟨Set.subset_inter h₁.1 h₂.1, by intro x hx y hy z hz hhz; exact @h₁.2 x hx.1 y hy.1 z hz hhz⟩ ->>>>>>> 328bba35178d0395ef45eb7cd046e70a98b161de -theorem map {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective f) (F C : ConvexSet R M) - (hF : F.IsFaceOf C) : - (F.map hhf).IsFaceOf (C.map hhf) := by - constructor - · have hF1 := hF.1 - intro x hx - rcases hx with ⟨y , hy, rfl⟩ - have hy1 : y ∈ C.carrier := Set.mem_of_mem_of_subset hy hF1 - apply Set.mem_image_of_mem - use hy1 - · intro x hx y hy z hz hhz - rcases hx with ⟨m , hmC, rfl⟩ - rcases hy with ⟨n , hnC, rfl⟩ - rcases hz with ⟨l , hlF, rfl⟩ - have hl : l ∈ Convexity.openSegment R m n := by - rcases hhz with ⟨ a, b, ha, hb, hab, hcomb⟩ - have h : f (convexCombPair a b ha.le hb.le hab m n) = - convexCombPair a b ha.le hb.le hab (f m) (f n) := hhf.map_convexCombPair ha.le hb.le hab m n - have hh : f (convexCombPair a b ha.le hb.le hab m n) = f l := by - simpa [h] using hcomb - exact ⟨ a, b, ha, hb, hab, hf hh⟩ - have hF2 := hF.2 - specialize @hF2 m hmC n hnC l hlF hl - apply Set.mem_image_of_mem - use hF2 - -<<<<<<< HEAD -/- F is a face of C iff the image of F is a face of the image of C under and injective affine map -/ -======= -theorem map_short {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective f) +/- The image of a face under an injective affine map is a face. -/ +theorem map {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective f) (F C : ConvexSet R M) (hF : F.IsFaceOf C) : (F.map hhf).IsFaceOf (C.map hhf) := by constructor · intro x hx @@ -285,50 +118,49 @@ theorem map_short {f : M → N} (hhf : IsAffineMap R f) (hf : Function.Injective exact ⟨ a, b, ha, hb, hab, hf hh⟩ exact Set.mem_image_of_mem _ (@hF.2 m hmC n hnC l hlF hl) ->>>>>>> 328bba35178d0395ef45eb7cd046e70a98b161de -theorem isFaceOf_map_iff (f : M → N) (hhf : IsAffineMap R f) (hf : Function.Injective f) -(C F : ConvexSet R M):(F.map hhf).IsFaceOf (C.map hhf) ↔ F.IsFaceOf C := by - apply Iff.intro - · intro h - constructor - · have h₁ := h.1 - have h' := (Set.image_subset_image_iff hf).mp h₁ - use h' - · intro x hx y hy z hz hhz - have hx' : f x ∈ (C.map hhf) := Set.mem_image_of_mem f hx - have hy' : f y ∈ (C.map hhf) := Set.mem_image_of_mem f hy - have hz' : f z ∈ (F.map hhf) := Set.mem_image_of_mem f hz - have hhz' : f z ∈ Convexity.openSegment R (f x) (f y) := by - rcases hhz with ⟨ a, b, ha, hb, hab, hcomb⟩ - have hff : f (convexCombPair a b ha.le hb.le hab x y) = - convexCombPair a b ha.le hb.le hab (f x) (f y) := hhf.map_convexCombPair ha.le hb.le hab x y - rw [hcomb] at hff - unfold Convexity.openSegment - use a, b, ha, hb, hab - use hff.symm - have h2 := h.2 - specialize @h2 (f x) hx' (f y) hy' (f z) hz' hhz' - exact (Function.Injective.mem_set_image hf).mp h2 - · intro h - apply map R hhf hf F C h - +/- defiition of preimage of a convex set -/ def comap {f : M → N} (hf : IsAffineMap R f) (C : ConvexSet R N) : ConvexSet R M := { carrier := f ⁻¹' C.carrier, isConvexSet := by apply Convexity.IsConvexSet.preimage hf C.isConvexSet } -theorem of_comap_surjective {f : M → N} (hf : IsAffineMap R f) (hhf : Function.Surjective f) (F C : ConvexSet R N) -(hF : (F.comap hf).IsFaceOf (C.comap hf)) : F.IsFaceOf C := by +/- The preimage of a face is a face -/ +theorem comap_face {f : M → N} (hf : IsAffineMap R f) (F C : ConvexSet R N) + (hF : F.IsFaceOf C) : (F.comap hf).IsFaceOf (C.comap hf) := by constructor - · have hF1 := hF.1 - have h1 : f '' (F.comap hf).carrier = F.carrier := by - apply Set.image_preimage_eq F hhf - have h2 : f '' (C.comap hf).carrier = C.carrier := by - apply Set.image_preimage_eq C hhf - have hF1' : f '' (F.comap hf).carrier ⊆ f '' (C.comap hf).carrier := by - sorry + · apply Set.preimage_mono hF.1 · have hF1 := hF.2 - - sorry + intro x hx y hy z hz hhz + have hhz' : f z ∈ Convexity.openSegment R (f x) (f y) := by + rcases hhz with ⟨ a, b, ha, hb, hab, hcomb⟩ + have hff : f (convexCombPair a b ha.le hb.le hab x y) = + convexCombPair a b ha.le hb.le hab (f x) (f y) := hf.map_convexCombPair ha.le hb.le hab x y + rw [hcomb] at hff + use a, b, ha, hb, hab, hff.symm + specialize @hF1 (f x) (Set.mem_preimage.mp hx ) (f y) (Set.mem_preimage.mp hy) (f z) ( + Set.mem_preimage.mp hz) hhz' + apply Set.mem_preimage.mp hF1 + +/- F is a face of C iff the image of F is a face of the image of C under an injective affine map -/ +theorem isFaceOf_map_iff_2 (f : M → N) (hhf : IsAffineMap R f) (hf : Function.Injective f) +(C F : ConvexSet R M):(F.map hhf).IsFaceOf (C.map hhf) ↔ F.IsFaceOf C := by + apply Iff.intro + · intro h + have hh:= comap_face R hhf (F.map hhf) (C.map hhf) h + have h (A: ConvexSet R M) : (A.map hhf).comap hhf = A := by + ext z + constructor + · intro hz + rcases hz with ⟨y, hy, hzy⟩ + rw [hf hzy] at hy + use hy + · intro hz + have hhz : f z ∈ (A.map hhf) := by + use z, hz + apply Set.mem_preimage.mp hhz + rw [h F, h C] at hh + exact hh + · intro h + apply map R hhf hf F C h end ConvexSet From 707fbf67d996b80309ccb7ee09cd1badf92432ff Mon Sep 17 00:00:00 2001 From: VTC Date: Tue, 30 Jun 2026 06:09:54 +0200 Subject: [PATCH 11/11] hopfully final version --- Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean index f55254e9..0ade774c 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/Face/Basic.lean @@ -142,7 +142,7 @@ theorem comap_face {f : M → N} (hf : IsAffineMap R f) (F C : ConvexSet R N) apply Set.mem_preimage.mp hF1 /- F is a face of C iff the image of F is a face of the image of C under an injective affine map -/ -theorem isFaceOf_map_iff_2 (f : M → N) (hhf : IsAffineMap R f) (hf : Function.Injective f) +theorem isFaceOf_map_iff (f : M → N) (hhf : IsAffineMap R f) (hf : Function.Injective f) (C F : ConvexSet R M):(F.map hhf).IsFaceOf (C.map hhf) ↔ F.IsFaceOf C := by apply Iff.intro · intro h