Grace/Cumulus/Topology/CompactImage.g17

Open in Workbench Download source

Imports

Compact · Set.Choice

Declarations

Source

1-- The continuous image of a compact set is compact: pull a cover back,2-- take a finite subcover, and push each member forward through a chosen3-- original. The choice of originals is the one use of choice in the4-- compactness development5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Topology.CompactImage11import Compact12import Set.Choice1314defgraph originalMap (f X C F : Set) (U ∈ F) : C := choose(originals(f, X, C, U))15requires inside : F ⊆ preimages(f, X, C)16proof17  have hU := inside with U, assumption18  obtain ⟨V, hV, shape⟩ := preimages.membership.forward with hU19  have original : V ∈ originals(f, X, C, U) := originals.membership.backward with ⟨hV, shape⟩20  have inhabited : Nonempty(originals(f, X, C, U)) := ⟨V, original⟩21  have chosen := choose.member with inhabited22  have parts := originals.membership.forward with chosen23  exact parts.left2425theorem IsCompact.image (f X T Y S A : Set)26  requires continuous : ContinuousMap(f, X, T, Y, S)27  requires compact : IsCompact(X, T, A)28  shows IsCompact(Y, S, functionImage(f, A, Y))29proof30  have function := continuous.left31  constructor32  . exact functionImage.subset at f, A, Y33  . intros D cover34    have pulledOpen : preimages(f, X, D) ⊆ T35      intros U hU36      obtain ⟨V, hV, shape⟩ := preimages.membership.forward with hU37      rw ← shape38      exact continuous.right with V, (cover.left with V, hV)39    have pulledCover : A ⊆ ⋃(preimages(f, X, D))40      intros a ha41      have haX := compact.left with a, ha42      have value := FunctionBetween.apply_closed with function, haX43      have imageMember : f(a) ∈ functionImage(f, A, Y) by simp [functionImage.membership]44      have covered := cover.right with f(a), imageMember45      obtain ⟨V, hV, inV⟩ := union.membership.forward with covered46      have member : functionPreimage(f, X, V) ∈ preimages(f, X, D) := preimages.membership.backward with ⟨V, hV, rfl⟩47      have inPreimage : a ∈ functionPreimage(f, X, V) := functionPreimage.membership.backward with ⟨haX, inV⟩48      exact union.contains with member, inPreimage49    obtain ⟨F, hF, finiteF, coveredA⟩ := compact.right with preimages(f, X, D), ⟨pulledOpen, pulledCover⟩50    have graph := originalMap.function with hF51    witness functionImage(originalMap(f, X, D, F), F, D)52    refine ⟨(functionImage.subset at originalMap(f, X, D, F), F, D), (Finite.function_image with graph, finiteF, (Subset.reflexive at F)), ?_⟩53    intros y hy54    simp [functionImage.membership] at hy55    obtain ⟨hyY, a, ha, shape⟩ := hy56    have covered := coveredA with a, ha57    obtain ⟨U, hU, haU⟩ := union.membership.forward with covered58    have value := originalMap.value with hF59    have hUP := hF with U, hU60    obtain ⟨V, hV, preimageShape⟩ := preimages.membership.forward with hUP61    have member : V ∈ originals(f, X, D, U) := originals.membership.backward with ⟨hV, preimageShape⟩62    have inhabited : Nonempty(originals(f, X, D, U)) := ⟨V, member⟩63    have chosen := choose.member with inhabited64    have chosenParts := originals.membership.forward with chosen65    rw ← value at chosenParts66    have inChosen : a ∈ functionPreimage(f, X, originalMap(f, X, D, F)(U)) by rwa chosenParts.right67    have hit := functionPreimage.membership.forward with inChosen68    have chosenMember : originalMap(f, X, D, F)(U) ∈ functionImage(originalMap(f, X, D, F), F, D)69      have closed := FunctionBetween.apply_closed with graph, hU70      simp [functionImage.membership]71      constructor72      . exact closed73      . witness U74        constructor75        . exact hU76        . rfl77    rw shape78    exact union.contains with chosenMember, hit.right79