Grace/Cumulus/Topology/Tube.g17

Open in Workbench Download source

Imports

Separation · Cardinal.FiniteUnion · Set.Choice

Declarations

Source

1-- The tube lemma and the compactness of a product: if A is compact in X2-- and B is compact in Y, then A × B is compact in the product topology.3-- Every open cover refines to open boxes; over each point of A finitely4-- many boxes cover the slice, and their widths meet in a tube; finitely5-- many tubes cover A.6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Topology.Tube12import Separation13import Cardinal.FiniteUnion14import Set.Choice1516-- Open boxes that sit inside some member of the cover C.17def innerBoxes (X T Y S C : Set) : Set :=18  { Z ∈ 𝒫(X × Y) | ∃ U ∈ T, ∃ V ∈ S, Z = U × V ∧ ∃ W ∈ C, Z ⊆ W }1920theorem innerBoxes.cover (X T Y S C A B : Set)21  requires topologyX : IsTopology(X, T)22  requires topologyY : IsTopology(Y, S)23  requires cover : OpenCover(productTopology(X, T, Y, S), A × B, C)24  shows A × B ⊆ ⋃(innerBoxes(X, T, Y, S, C))25proof26  intros p hp27  obtain ⟨W, hW, hpW⟩ := union.membership.forward with (cover.right with p, hp)28  have parts := productTopology.membership.forward with (cover.left with W, hW)29  obtain ⟨U, hU, V, hV, inBox, boxInside⟩ := parts.right with p, hpW30  have inside := product.monotone with (IsTopology.subset with topologyX, hU), (IsTopology.subset with topologyY, hV)31  have member : U × V ∈ innerBoxes(X, T, Y, S, C)32    exact innerBoxes.membership.backward with ⟨(powerset.membership_iff.backward with inside), U, hU, V, hV, rfl, W, hW, boxInside⟩33  exact union.contains with member, inBox3435-- A finite family of inner boxes gives a finite subfamily of C.36def boxOrigins (C Z : Set) : Set := { W ∈ C | Z ⊆ W }3738defgraph boxOrigin (X T Y S C G : Set) (Z ∈ G) : C := choose(boxOrigins(C, Z))39requires inner : G ⊆ innerBoxes(X, T, Y, S, C)40proof41  have hZ := inner with Z, assumption42  have parts := innerBoxes.membership.forward with hZ43  obtain ⟨U, hU, V, hV, shape, W, hW, inside⟩ := parts.right44  have original : W ∈ boxOrigins(C, Z) := boxOrigins.membership.backward with ⟨hW, inside⟩45  have inhabited : Nonempty(boxOrigins(C, Z)) := ⟨W, original⟩46  have chosen := choose.member with inhabited47  have chosenParts := boxOrigins.membership.forward with chosen48  exact chosenParts.left4950theorem Compact.of_inner_boxes (X T Y S C G A B : Set)51  requires inner : G ⊆ innerBoxes(X, T, Y, S, C)52  requires finite : Finite(G)53  requires covers : A × B ⊆ ⋃(G)54  shows ∃ F, F ⊆ C ∧ Finite(F) ∧ A × B ⊆ ⋃(F)55proof56  have graph := boxOrigin.function with inner57  witness functionImage(boxOrigin(X, T, Y, S, C, G), G, C)58  refine ⟨(functionImage.subset at boxOrigin(X, T, Y, S, C, G), G, C), (Finite.function_image with graph, finite, (Subset.reflexive at G)), ?_⟩59  intros p hp60  obtain ⟨Z, hZ, hpZ⟩ := union.membership.forward with (covers with p, hp)61  have value := boxOrigin.value with inner62  have hZInner := inner with Z, hZ63  have parts := innerBoxes.membership.forward with hZInner64  obtain ⟨U, hU, V, hV, shape, W, hW, inside⟩ := parts.right65  have original : W ∈ boxOrigins(C, Z) := boxOrigins.membership.backward with ⟨hW, inside⟩66  have inhabited : Nonempty(boxOrigins(C, Z)) := ⟨W, original⟩67  have chosen := choose.member with inhabited68  have chosenParts := boxOrigins.membership.forward with chosen69  rw ← value at chosenParts70  have member : boxOrigin(X, T, Y, S, C, G)(Z) ∈ functionImage(boxOrigin(X, T, Y, S, C, G), G, C)71    have closed := FunctionBetween.apply_closed with graph, hZ72    simp [functionImage.membership]73    constructor74    . exact closed75    . witness Z76      constructor77      . exact hZ78      . rfl79  exact union.contains with member, (chosenParts.right with p, hpZ)8081-- Over a point x of A: the slices of the boxes through x cover B.82def slices (T S G x : Set) : Set := { V ∈ S | ∃ U ∈ T, U × V ∈ G ∧ x ∈ U }8384theorem slices.cover (X T Y S C A B x : Set)85  requires hx : x ∈ A86  requires covers : A × B ⊆ ⋃(innerBoxes(X, T, Y, S, C))87  shows B ⊆ ⋃(slices(T, S, innerBoxes(X, T, Y, S, C), x))88proof89  intros y hy90  have pair := product.pair with hx, hy91  obtain ⟨Z, hZ, hpZ⟩ := union.membership.forward with (covers with (x, y), pair)92  have parts := innerBoxes.membership.forward with hZ93  obtain ⟨U, hU, V, hV, shape, W, hW, inside⟩ := parts.right94  rw shape at hpZ95  have coordinates := product.pair_membership.forward with hpZ96  rw shape at hZ97  have member : V ∈ slices(T, S, innerBoxes(X, T, Y, S, C), x)98    exact slices.membership.backward with ⟨hV, U, hU, hZ, coordinates.left⟩99  exact union.contains with member, coordinates.right100101-- Finitely many slices cover B; each slice has a chosen width through x.102def sliceCovers (T S G x B : Set) : Set :=103  { F ∈ 𝒫(slices(T, S, G, x)) | Finite(F) ∧ B ⊆ ⋃(F) }104def sliceCover (T S G x B : Set) : Set := choose(sliceCovers(T, S, G, x, B))105def widthCandidates (T G x V : Set) : Set := { U ∈ T | U × V ∈ G ∧ x ∈ U }106def width (T G x V : Set) : Set := choose(widthCandidates(T, G, x, V))107108theorem sliceCover.selected (Y T S G x B : Set)109  requires compact : IsCompact(Y, S, B)110  requires covers : B ⊆ ⋃(slices(T, S, G, x))111  shows sliceCover(T, S, G, x, B) ⊆ slices(T, S, G, x) ∧ Finite(sliceCover(T, S, G, x, B)) ∧112    B ⊆ ⋃(sliceCover(T, S, G, x, B))113proof114  have slicesOpen : slices(T, S, G, x) ⊆ S115    intros V hV116    have parts := slices.membership.forward with hV117    exact parts.left118  obtain ⟨F, hF, finiteF, coveredB⟩ := compact.right with slices(T, S, G, x), ⟨slicesOpen, covers⟩119  have member : F ∈ sliceCovers(T, S, G, x, B)120    exact sliceCovers.membership.backward with ⟨(powerset.membership_iff.backward with hF), finiteF, coveredB⟩121  have inhabited : Nonempty(sliceCovers(T, S, G, x, B)) := ⟨F, member⟩122  have chosen := choose.member with inhabited123  have same : sliceCover(T, S, G, x, B) = choose(sliceCovers(T, S, G, x, B))124    unfold sliceCover125    rfl126  rw same127  have parts := sliceCovers.membership.forward with chosen128  have rest := parts.right129  refine ⟨(powerset.membership_iff.forward with parts.left), rest.left, rest.right⟩130131theorem width.selected (T S G x V : Set)132  requires hV : V ∈ slices(T, S, G, x)133  shows width(T, G, x, V) ∈ T ∧ width(T, G, x, V) × V ∈ G ∧ x ∈ width(T, G, x, V)134proof135  have parts := slices.membership.forward with hV136  obtain ⟨U, hU, boxIn, hxU⟩ := parts.right137  have candidate : U ∈ widthCandidates(T, G, x, V) := widthCandidates.membership.backward with ⟨hU, boxIn, hxU⟩138  have inhabited : Nonempty(widthCandidates(T, G, x, V)) := ⟨U, candidate⟩139  have chosen := choose.member with inhabited140  have same : width(T, G, x, V) = choose(widthCandidates(T, G, x, V))141    unfold width142    rfl143  rw same144  exact widthCandidates.membership.forward with chosen145146-- The widths of the chosen slices meet in the tube over x.147defgraph widthMap (T S G x B : Set) (V ∈ sliceCover(T, S, G, x, B)) : T := width(T, G, x, V)148requires inner : sliceCover(T, S, G, x, B) ⊆ slices(T, S, G, x)149proof150  have hV := inner with V, assumption151  have selected := width.selected with hV152  exact selected.left153154def widths (T S G x B : Set) : Set :=155  functionImage(widthMap(T, S, G, x, B), sliceCover(T, S, G, x, B), T)156def tube (T S G x B : Set) : Set := ⋂(widths(T, S, G, x, B))157158theorem widths.membership (U T S G x B : Set)159  requires inner : sliceCover(T, S, G, x, B) ⊆ slices(T, S, G, x)160  shows U ∈ widths(T, S, G, x, B) ↔ ∃ V ∈ sliceCover(T, S, G, x, B), U = width(T, G, x, V)161proof162  have same : widths(T, S, G, x, B) = functionImage(widthMap(T, S, G, x, B), sliceCover(T, S, G, x, B), T)163    unfold widths164    rfl165  rw same166  constructor167  . intro hU168    simp [functionImage.membership] at hU169    obtain ⟨inT, V, hV, shape⟩ := hU170    have value := widthMap.value with inner171    rw value at shape172    refine ⟨V, hV, shape⟩173  . intro represented174    obtain ⟨V, hV, shape⟩ := represented175    have value := widthMap.value with inner176    have selected := width.selected with (inner with V, hV)177    rw [shape, ← value]178    have graph := widthMap.function with inner179    have closed := FunctionBetween.apply_closed with graph, hV180    simp [functionImage.membership]181182theorem tube.open (X T S G x B : Set)183  requires topology : IsTopology(X, T)184  requires inner : sliceCover(T, S, G, x, B) ⊆ slices(T, S, G, x)185  requires finite : Finite(sliceCover(T, S, G, x, B))186  requires inhabited : Nonempty(sliceCover(T, S, G, x, B))187  shows tube(T, S, G, x, B) ∈ T188proof189  have graph := widthMap.function with inner190  obtain ⟨V, hV⟩ := inhabited191  have member : width(T, G, x, V) ∈ widths(T, S, G, x, B)192    apply widths.membership.backward with inner193    refine ⟨V, hV, rfl⟩194  have nonempty : Nonempty(widths(T, S, G, x, B)) := ⟨width(T, G, x, V), member⟩195  have finiteWidths : Finite(widths(T, S, G, x, B))196    unfold widths197    exact Finite.function_image with graph, finite, (Subset.reflexive at sliceCover(T, S, G, x, B))198  have inside : widths(T, S, G, x, B) ⊆ T199    unfold widths200    exact functionImage.subset201  unfold tube202  exact IsTopology.finite_intersection with topology, finiteWidths, inside, nonempty203204theorem tube.contains (T S G x B : Set)205  requires inner : sliceCover(T, S, G, x, B) ⊆ slices(T, S, G, x)206  requires inhabited : Nonempty(sliceCover(T, S, G, x, B))207  shows x ∈ tube(T, S, G, x, B)208proof209  obtain ⟨V, hV⟩ := inhabited210  have member : width(T, G, x, V) ∈ widths(T, S, G, x, B)211    apply widths.membership.backward with inner212    refine ⟨V, hV, rfl⟩213  have nonempty : Nonempty(widths(T, S, G, x, B)) := ⟨width(T, G, x, V), member⟩214  unfold tube215  apply familyIntersection.membership_of_nonempty.backward with nonempty216  intros U hU217  obtain ⟨V2, hV2, shape⟩ := widths.membership.forward with inner, hU218  rw shape219  have selected := width.selected with (inner with V2, hV2)220  have rest := selected.right221  exact rest.right222223theorem tube.width (T S G x B u V : Set)224  requires inner : sliceCover(T, S, G, x, B) ⊆ slices(T, S, G, x)225  requires hu : u ∈ tube(T, S, G, x, B)226  requires hV : V ∈ sliceCover(T, S, G, x, B)227  shows u ∈ width(T, G, x, V)228proof229  have member : width(T, G, x, V) ∈ widths(T, S, G, x, B)230    apply widths.membership.backward with inner231    refine ⟨V, hV, rfl⟩232  have nonempty : Nonempty(widths(T, S, G, x, B)) := ⟨width(T, G, x, V), member⟩233  unfold tube at hu234  have all := familyIntersection.membership_of_nonempty.forward with nonempty, hu235  exact all with width(T, G, x, V), member236237-- The boxes over the tube: one per chosen slice.238defgraph tubeBoxMap (X T Y S G x B : Set) (V ∈ sliceCover(T, S, G, x, B)) : 𝒫(X × Y) := width(T, G, x, V) × V239requires topologyX : IsTopology(X, T)240requires topologyY : IsTopology(Y, S)241requires inner : sliceCover(T, S, G, x, B) ⊆ slices(T, S, G, x)242proof243  have hV := inner with V, assumption244  have selected := width.selected with hV245  have sliceParts := slices.membership.forward with hV246  have widthInside := IsTopology.subset with topologyX, selected.left247  have sliceInside := IsTopology.subset with topologyY, sliceParts.left248  apply powerset.membership_iff.backward249  exact product.monotone with widthInside, sliceInside250251def tubeBoxes (X T Y S G x B : Set) : Set :=252  functionImage(tubeBoxMap(X, T, Y, S, G, x, B), sliceCover(T, S, G, x, B), 𝒫(X × Y))253254theorem tubeBoxes.finite (X T Y S G x B : Set)255  requires topologyX : IsTopology(X, T)256  requires topologyY : IsTopology(Y, S)257  requires inner : sliceCover(T, S, G, x, B) ⊆ slices(T, S, G, x)258  requires finite : Finite(sliceCover(T, S, G, x, B))259  shows Finite(tubeBoxes(X, T, Y, S, G, x, B))260proof261  have graph := tubeBoxMap.function with topologyX, topologyY, inner262  unfold tubeBoxes263  exact Finite.function_image with graph, finite, (Subset.reflexive at sliceCover(T, S, G, x, B))264265theorem tubeBoxes.inside (X T Y S G x B : Set)266  requires topologyX : IsTopology(X, T)267  requires topologyY : IsTopology(Y, S)268  requires inner : sliceCover(T, S, G, x, B) ⊆ slices(T, S, G, x)269  shows tubeBoxes(X, T, Y, S, G, x, B) ⊆ G270proof271  intros Z hZ272  unfold tubeBoxes at hZ273  simp [functionImage.membership] at hZ274  obtain ⟨bound, V, hV, shape⟩ := hZ275  have value := tubeBoxMap.value with topologyX, topologyY, inner276  rw [shape, value]277  have selected := width.selected with (inner with V, hV)278  have rest := selected.right279  exact rest.left280281theorem tube.covered (X T Y S G x B : Set)282  requires topologyX : IsTopology(X, T)283  requires topologyY : IsTopology(Y, S)284  requires inner : sliceCover(T, S, G, x, B) ⊆ slices(T, S, G, x)285  requires covers : B ⊆ ⋃(sliceCover(T, S, G, x, B))286  shows tube(T, S, G, x, B) × B ⊆ ⋃(tubeBoxes(X, T, Y, S, G, x, B))287proof288  have graph := tubeBoxMap.function with topologyX, topologyY, inner289  intros p hp290  obtain ⟨bound, u, hu, y, hy, shape⟩ := product.membership.forward with hp291  obtain ⟨V, hV, hyV⟩ := union.membership.forward with (covers with y, hy)292  have inWidth := tube.width with inner, hu, hV293  have value := tubeBoxMap.value with topologyX, topologyY, inner294  have member : width(T, G, x, V) × V ∈ tubeBoxes(X, T, Y, S, G, x, B)295    unfold tubeBoxes296    have closed := FunctionBetween.apply_closed with graph, hV297    rw ← value298    simp [functionImage.membership]299    constructor300    . exact closed301    . witness V302      constructor303      . exact hV304      . rfl305  rw shape306  exact union.contains with member, (product.pair with inWidth, hyV)307308-- Finitely many tubes cover A; their boxes form a finite subfamily of G.309def tubes (T S G A B : Set) : Set := { tube(T, S, G, x, B) | x ∈ A }310def tubeOrigins (T S G A B N : Set) : Set := { x ∈ A | tube(T, S, G, x, B) = N }311312defgraph tubeOrigin (T S G A B F : Set) (N ∈ F) : A := choose(tubeOrigins(T, S, G, A, B, N))313requires inside : F ⊆ tubes(T, S, G, A, B)314proof315  have hN := inside with N, assumption316  obtain ⟨x, hx, shape⟩ := tubes.membership.forward with hN317  have original : x ∈ tubeOrigins(T, S, G, A, B, N) := tubeOrigins.membership.backward with ⟨hx, shape⟩318  have inhabited : Nonempty(tubeOrigins(T, S, G, A, B, N)) := ⟨x, original⟩319  have chosen := choose.member with inhabited320  have parts := tubeOrigins.membership.forward with chosen321  exact parts.left322323theorem tubeOrigin.tube (T S G A B F N : Set)324  requires inside : F ⊆ tubes(T, S, G, A, B)325  requires hN : N ∈ F326  shows tube(T, S, G, tubeOrigin(T, S, G, A, B, F)(N), B) = N327proof328  have hNT := inside with N, hN329  obtain ⟨x, hx, shape⟩ := tubes.membership.forward with hNT330  have original : x ∈ tubeOrigins(T, S, G, A, B, N) := tubeOrigins.membership.backward with ⟨hx, shape⟩331  have inhabited : Nonempty(tubeOrigins(T, S, G, A, B, N)) := ⟨x, original⟩332  have chosen := choose.member with inhabited333  have parts := tubeOrigins.membership.forward with chosen334  have value := tubeOrigin.value with inside335  rw value336  exact parts.right337338defgraph tubeBoxFamily (X T Y S G A B F : Set) (N ∈ F) : 𝒫(𝒫(X × Y)) :=339  tubeBoxes(X, T, Y, S, G, tubeOrigin(T, S, G, A, B, F)(N), B)340requires inside : F ⊆ tubes(T, S, G, A, B)341proof342  apply powerset.membership_iff.backward343  unfold tubeBoxes344  exact functionImage.subset345346-- The product of compact sets is compact.347theorem IsCompact.product (X T Y S A B : Set)348  requires topologyX : IsTopology(X, T)349  requires topologyY : IsTopology(Y, S)350  requires compactA : IsCompact(X, T, A)351  requires compactB : IsCompact(Y, S, B)352  shows IsCompact(X × Y, productTopology(X, T, Y, S), A × B)353proof354  have hA := compactA.left355  have hB := compactB.left356  constructor357  . exact product.monotone with hA, hB358  . intros C cover359    have split : Nonempty(B) ∨ ¬Nonempty(B) by tauto360    cases split with inhabitedB | emptyB361    . have boxesCover := innerBoxes.cover with topologyX, topologyY, cover362      -- the facts about every point of A363      have sliceFacts : ∀ x ∈ A,364          sliceCover(T, S, innerBoxes(X, T, Y, S, C), x, B) ⊆ slices(T, S, innerBoxes(X, T, Y, S, C), x) ∧365          Finite(sliceCover(T, S, innerBoxes(X, T, Y, S, C), x, B)) ∧366          B ⊆ ⋃(sliceCover(T, S, innerBoxes(X, T, Y, S, C), x, B))367        intros x hx368        have slicesCover := slices.cover with hx, boxesCover369        exact sliceCover.selected with compactB, slicesCover370      have nonemptyCovers : ∀ x ∈ A, Nonempty(sliceCover(T, S, innerBoxes(X, T, Y, S, C), x, B))371        intros x hx372        obtain ⟨inner, finite, covers⟩ := sliceFacts with x, hx373        obtain ⟨y, hy⟩ := inhabitedB374        obtain ⟨V, hV, hyV⟩ := union.membership.forward with (covers with y, hy)375        exact ⟨V, hV⟩376      have tubesOpen : tubes(T, S, innerBoxes(X, T, Y, S, C), A, B) ⊆ T377        intros N hN378        obtain ⟨x, hx, shape⟩ := tubes.membership.forward with hN379        obtain ⟨inner, finite, covers⟩ := sliceFacts with x, hx380        rw ← shape381        exact tube.open with topologyX, inner, finite, (nonemptyCovers with x, hx)382      have tubesCover : A ⊆ ⋃(tubes(T, S, innerBoxes(X, T, Y, S, C), A, B))383        intros x hx384        obtain ⟨inner, finite, covers⟩ := sliceFacts with x, hx385        have member : tube(T, S, innerBoxes(X, T, Y, S, C), x, B) ∈ tubes(T, S, innerBoxes(X, T, Y, S, C), A, B)386          exact tubes.membership.backward with ⟨x, hx, rfl⟩387        exact union.contains with member, (tube.contains with inner, (nonemptyCovers with x, hx))388      obtain ⟨F, hF, finiteF, coveredA⟩ := compactA.right with tubes(T, S, innerBoxes(X, T, Y, S, C), A, B), ⟨tubesOpen, tubesCover⟩389      have familyGraph := tubeBoxFamily.function at X, T, Y, S, innerBoxes(X, T, Y, S, C), A, B, F with hF390      have originGraph := tubeOrigin.function with hF391      -- the finite family of boxes392      have familyFinite := Finite.function_image with familyGraph, finiteF, (Subset.reflexive at F)393      have membersFinite : ∀ H ∈ functionImage(tubeBoxFamily(X, T, Y, S, innerBoxes(X, T, Y, S, C), A, B, F), F, 𝒫(𝒫(X × Y))), Finite(H)394        intros H hH395        simp [functionImage.membership] at hH396        obtain ⟨bound, N, hN, shape⟩ := hH397        have value := tubeBoxFamily.value at X, T, Y, S, innerBoxes(X, T, Y, S, C), A, B, F, N with hF398        rw [shape, value]399        have origin := FunctionBetween.apply_closed with originGraph, hN400        obtain ⟨inner, finite, covers⟩ := sliceFacts with tubeOrigin(T, S, innerBoxes(X, T, Y, S, C), A, B, F)(N), origin401        exact tubeBoxes.finite with topologyX, topologyY, inner, finite402      have unionFinite := Finite.big_union with familyFinite, membersFinite403      have unionInside : ⋃(functionImage(tubeBoxFamily(X, T, Y, S, innerBoxes(X, T, Y, S, C), A, B, F), F, 𝒫(𝒫(X × Y)))) ⊆ innerBoxes(X, T, Y, S, C)404        apply union.subset405        intros H hH406        simp [functionImage.membership] at hH407        obtain ⟨bound, N, hN, shape⟩ := hH408        have value := tubeBoxFamily.value at X, T, Y, S, innerBoxes(X, T, Y, S, C), A, B, F, N with hF409        rw [shape, value]410        have origin := FunctionBetween.apply_closed with originGraph, hN411        obtain ⟨inner, finite, covers⟩ := sliceFacts with tubeOrigin(T, S, innerBoxes(X, T, Y, S, C), A, B, F)(N), origin412        exact tubeBoxes.inside with topologyX, topologyY, inner413      have unionCovers : A × B ⊆ ⋃(⋃(functionImage(tubeBoxFamily(X, T, Y, S, innerBoxes(X, T, Y, S, C), A, B, F), F, 𝒫(𝒫(X × Y)))))414        intros p hp415        obtain ⟨bound, a, ha, y, hy, shape⟩ := product.membership.forward with hp416        obtain ⟨N, hN, haN⟩ := union.membership.forward with (coveredA with a, ha)417        have origin := FunctionBetween.apply_closed with originGraph, hN418        have tubeShape := tubeOrigin.tube with hF, hN419        obtain ⟨inner, finite, covers⟩ := sliceFacts with tubeOrigin(T, S, innerBoxes(X, T, Y, S, C), A, B, F)(N), origin420        have covered := tube.covered with topologyX, topologyY, inner, covers421        rw tubeShape at covered422        have inTube : (a, y) ∈ N × B := product.pair with haN, hy423        obtain ⟨Z, hZ, hpZ⟩ := union.membership.forward with (covered with (a, y), inTube)424        have value := tubeBoxFamily.value at X, T, Y, S, innerBoxes(X, T, Y, S, C), A, B, F, N with hF425        have familyMember : tubeBoxFamily(X, T, Y, S, innerBoxes(X, T, Y, S, C), A, B, F)(N) ∈ functionImage(tubeBoxFamily(X, T, Y, S, innerBoxes(X, T, Y, S, C), A, B, F), F, 𝒫(𝒫(X × Y)))426          have closed := FunctionBetween.apply_closed with familyGraph, hN427          simp [functionImage.membership]428          constructor429          . exact closed430          . witness N431            constructor432            . exact hN433            . rfl434        rw value at familyMember435        have inUnion := union.contains with familyMember, hZ436        rw shape437        exact union.contains with inUnion, hpZ438      exact Compact.of_inner_boxes with unionInside, unionFinite, unionCovers439    . have bEmpty : B = ∅440        by_contra different441        apply emptyB442        exact Nonempty.of_ne_empty with different443      rw under bEmpty444      rw under product.right_empty445      witness ∅446      refine ⟨(empty.subset at C), Finite.empty, (empty.subset at ⋃(∅))⟩447