Grace/Cumulus/Set/Involution.g17

Open in Workbench Download source

Imports

Function

Declarations

Source

1-- Involutions and restriction to unions of their orbits (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Set.Involution8import Function910predicate InvolutionOn (t D : Set) := FunctionBetween(t, D, D) ∧ (∀ x ∈ D, t(t(x)) = x)1112theorem InvolutionOn.function (t D : Set)13  requires involution : InvolutionOn(t, D)14  shows t : D → D15proof16  simp [InvolutionOn]1718theorem InvolutionOn.apply (t D x : Set)19  requires involution : InvolutionOn(t, D)20  requires member : x ∈ D21  shows t(t(x)) = x22proof23  ext y24  simp [InvolutionOn]2526theorem InvolutionOn.bijective (t D : Set)27  requires involution : InvolutionOn(t, D)28  shows BijectiveBetween(t, D, D)29proof30  have function := InvolutionOn.function with involution31  constructor32  . unfold InjectiveBetween33    refine ⟨function, ?_⟩34    intros x hx y hy z hz first second35    have tx := FunctionBetween.apply_value with function, hx, first36    have ty := FunctionBetween.apply_value with function, hy, second37    have inverseX := InvolutionOn.apply with involution, hx38    have inverseY := InvolutionOn.apply with involution, hy39    cc40  . unfold SurjectiveBetween41    refine ⟨function, ?_⟩42    intros y hy43    have image := FunctionBetween.apply_closed with function, hy44    have inverse := InvolutionOn.apply with involution, hy45    have graph := FunctionBetween.relates_apply with function, image46    refine ⟨t(y), image, ?_⟩47    rwa inverse at graph4849theorem InvolutionOn.remove_pair (t D V a : Set)50  requires involution : InvolutionOn(t, D)51  requires subset : V ⊆ D52  requires closed : ∀ x ∈ V, t(x) ∈ V53  requires member : a ∈ V54  shows ∀ x ∈ (V ∖ {a}) ∖ {t(a)}, t(x) ∈ (V ∖ {a}) ∖ {t(a)}55proof56  have aIn := subset with a, member57  have inverseA := InvolutionOn.apply with involution, aIn58  intros x hx59  have outer := difference.membership.forward with hx60  have inner := difference.membership.forward with outer.left61  have xIn := subset with x, inner.left62  have inverseX := InvolutionOn.apply with involution, xIn63  have image := closed with x, inner.left64  have notA : ¬(t(x) ∈ {a})65    intro singleton66    have equal := singleton.membership.forward with singleton67    have same : x = t(a) by cc68    have forbidden : x ∈ {t(a)} by simp69    exact outer.right with forbidden70  have notPartner : ¬(t(x) ∈ {t(a)})71    intro singleton72    have equal := singleton.membership.forward with singleton73    have same : x = a by cc74    have forbidden : x ∈ {a} by simp75    exact inner.right with forbidden76  exact difference.membership.backward with ⟨(difference.membership.backward with ⟨image, notA⟩), notPartner⟩7778-- Restrict an involution when it exchanges two (possibly overlapping) subsets.79theorem InvolutionOn.restrict_between (t D S T : Set)80  requires involution : InvolutionOn(t, D)81  requires subsetS : S ⊆ D82  requires subsetT : T ⊆ D83  requires forward : ∀ x ∈ S, t(x) ∈ T84  requires backward : ∀ y ∈ T, t(y) ∈ S85  shows BijectiveBetween(restrict(t, S), S, T)86proof87  have function := InvolutionOn.function with involution88  have restricted := restrict.function at t, D, D, S, T with *89  constructor90  . unfold InjectiveBetween91    refine ⟨restricted, ?_⟩92    intros x hx y hy z hz first second93    have valueX := FunctionBetween.apply_value with restricted, hx, first94    have valueY := FunctionBetween.apply_value with restricted, hy, second95    have restrictedX := restrict.apply with hx96    have restrictedY := restrict.apply with hy97    have xIn := subsetS with x, hx98    have yIn := subsetS with y, hy99    have inverseX := InvolutionOn.apply with involution, xIn100    have inverseY := InvolutionOn.apply with involution, yIn101    cc102  . unfold SurjectiveBetween103    refine ⟨restricted, ?_⟩104    intros y hy105    have preimage := backward with y, hy106    have yIn := subsetT with y, hy107    have inverse := InvolutionOn.apply with involution, yIn108    have value := restrict.apply at t, D, D, S, T, t(y) with *109    have graph := FunctionBetween.relates_apply with restricted, preimage110    refine ⟨t(y), preimage, ?_⟩111    have same : restrict(t, S)(t(y)) = y by cc112    rwa same at graph113