diff --git a/build.sbt b/build.sbt index 4a3136c13..9f3699142 100644 --- a/build.sbt +++ b/build.sbt @@ -1,4 +1,4 @@ -ThisBuild / version := "0.7" +ThisBuild / version := "0.7" ThisBuild / homepage := Some(url("https://github.com/epfl-lara/lisa")) ThisBuild / startYear := Some(2021) ThisBuild / organization := "ch.epfl.lara" @@ -7,10 +7,10 @@ ThisBuild / organizationHomepage := Some(url("https://lara.epfl.ch")) ThisBuild / licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.html")) ThisBuild / versionScheme := Some("semver-spec") ThisBuild / scalacOptions ++= Seq( - "-feature", - "-deprecation", - "-unchecked", - ) + "-feature", + "-deprecation", + "-unchecked" +) ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8") ThisBuild / semanticdbEnabled := true ThisBuild / semanticdbVersion := scalafixSemanticdb.revision @@ -19,7 +19,6 @@ val scala2 = "2.13.8" val scala3 = "3.5.1" val commonSettings = Seq( crossScalaVersions := Seq(scala3), - run / fork := true ) @@ -31,9 +30,8 @@ val commonSettings3 = commonSettings ++ Seq( scalaVersion := scala3, scalacOptions ++= Seq( "-language:implicitConversions", - //"-rewrite", "-source", "3.4-migration", + // "-rewrite", "-source", "3.4-migration", "-Wconf:msg=.*will never be selected.*:silent" - ), javaOptions += "-Xmx10G", libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.18" % "test", @@ -50,9 +48,9 @@ def githubProject(repo: String, commitHash: String) = RootProject(uri(s"$repo#$c lazy val customTstpParser = githubProject("https://github.com/SimonGuilloud/scala-tptp-parser.git", "eae9c1b7a9546f74779d77ff50fa6e8a1654cfa0") lazy val root = Project( - id = "lisa", - base = file("."), - ) + id = "lisa", + base = file(".") +) .settings(commonSettings3) .dependsOn(kernel, withTests(utils), withTests(sets)) // Everything but `examples` .aggregate(utils) // To run tests on all modules @@ -75,17 +73,26 @@ lazy val sets = Project( .settings(commonSettings3) .dependsOn(kernel, withTests(utils)) +lazy val topologies = Project( + id = "lisa-topology", + base = file("lisa-topology") +) + .settings(commonSettings3) + .dependsOn(kernel, sets, withTests(utils)) + lazy val utils = Project( id = "lisa-utils", base = file("lisa-utils") ) - .settings(commonSettings3 ++ Seq( - libraryDependencies += "ch.epfl.lara" %% "scallion" % "0.6" from "https://github.com/epfl-lara/scallion/releases/download/v0.6/scallion_3-0.6.jar", - libraryDependencies += "ch.epfl.lara" %% "silex" % "0.6" from "https://github.com/epfl-lara/silex/releases/download/v0.6/silex_3-0.6.jar", - )) + .settings( + commonSettings3 ++ Seq( + libraryDependencies += "ch.epfl.lara" %% "scallion" % "0.6" from "https://github.com/epfl-lara/scallion/releases/download/v0.6/scallion_3-0.6.jar", + libraryDependencies += "ch.epfl.lara" %% "silex" % "0.6" from "https://github.com/epfl-lara/silex/releases/download/v0.6/silex_3-0.6.jar" + ) + ) .dependsOn(kernel) .dependsOn(customTstpParser) - //.settings(libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4") +//.settings(libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4") ThisBuild / assemblyMergeStrategy := { case PathList("module-info.class") => MergeStrategy.discard @@ -97,7 +104,6 @@ ThisBuild / assemblyMergeStrategy := { oldStrategy(x) } - lazy val examples = Project( id = "lisa-examples", base = file("lisa-examples") diff --git a/lisa-sets/src/main/scala/lisa/automation/Congruence.scala b/lisa-sets/src/main/scala/lisa/automation/Congruence.scala index 8c60de410..137f4279b 100644 --- a/lisa-sets/src/main/scala/lisa/automation/Congruence.scala +++ b/lisa-sets/src/main/scala/lisa/automation/Congruence.scala @@ -1,11 +1,11 @@ package lisa.automation +import leo.datastructures.TPTP.CNF.AtomicFormula import lisa.fol.FOL.{*, given} import lisa.prooflib.BasicStepTactic.* import lisa.prooflib.ProofTacticLib.* import lisa.prooflib.SimpleDeducedSteps.* import lisa.prooflib.* import lisa.utils.parsing.UnreachableException -import leo.datastructures.TPTP.CNF.AtomicFormula /** * This tactic tries to prove a sequent by congruence. diff --git a/lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala b/lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala index 651a3f7a1..ea330eb9d 100644 --- a/lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala +++ b/lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala @@ -2,6 +2,7 @@ package lisa.automation.settheory import lisa.SetTheoryLibrary.{_, given} import lisa.automation.Tautology +import lisa.automation.kernel.CommonTactics.ExistenceAndUniqueness import lisa.fol.FOL.{_, given} import lisa.kernel.proof.SequentCalculus as SCunique import lisa.maths.Quantifiers @@ -21,8 +22,10 @@ object SetTheoryTactics { private val x = variable private val y = variable private val z = variable + private val v = variable private val h = formulaVariable private val P = predicate[1] + private val Q = predicate[1] private val schemPred = predicate[1] /** @@ -197,4 +200,99 @@ object SetTheoryTactics { unwrapTactic(sp)("Subproof for unique comprehension failed.") } } + + /** + * Defines the element that is uniquely given by the uniqueness theorem, or falls back to the error element if the + * assumptions of the theorem are not satisfied. + * + * This is useful in defining specific elements in groups, where their uniqueness (and existence) strongly rely + * on the assumption of the group structure. + */ + object TheConditional { + def apply(using om: OutputManager)(u: Variable, f: Formula)(just: JUSTIFICATION, defaultValue: Term = ∅): The = { + val seq = just.statement + + if (seq.left.isEmpty) { + The(u, f)(just) + } else { + val prem = if (seq.left.size == 1) seq.left.head else And(seq.left.toSeq) + val completeDef = (prem ==> f) /\ (!prem ==> (u === defaultValue)) + val substF = completeDef.substitute(u := defaultValue) + val substDef = completeDef.substitute(u := v) + + val completeUniquenessTheorem = Lemma( + ∃!(u, completeDef) + ) { + val case1 = have(prem |- ∃!(u, completeDef)) subproof { + // We prove the equivalence f <=> completeDef so that we can substitute it in the uniqueness quantifier + val equiv = have(prem |- ∀(u, f <=> completeDef)) subproof { + have(f |- f) by Hypothesis + thenHave((prem, f) |- f) by Weakening + val left = thenHave(f |- (prem ==> f)) by Restate + + have(prem |- prem) by Hypothesis + thenHave((prem, !prem) |- ()) by LeftNot + thenHave((prem, !prem) |- (u === defaultValue)) by Weakening + val right = thenHave(prem |- (!prem ==> (u === defaultValue))) by Restate + + have((prem, f) |- completeDef) by RightAnd(left, right) + val forward = thenHave(prem |- f ==> completeDef) by Restate + + have(completeDef |- completeDef) by Hypothesis + thenHave((prem, completeDef) |- completeDef) by Weakening + thenHave((prem, completeDef) |- f) by Tautology + val backward = thenHave(prem |- completeDef ==> f) by Restate + + have(prem |- f <=> completeDef) by RightIff(forward, backward) + thenHave(thesis) by RightForall + } + + val substitution = have((∃!(u, f), ∀(u, f <=> completeDef)) |- ∃!(u, completeDef)) by Tautology.from( + Quantifiers.uniqueExistentialEquivalenceDistribution of (P := lambda(u, f), Q := lambda(u, completeDef)) + ) + + val implication = have((prem, ∃!(u, f)) |- ∃!(u, completeDef)) by Cut(equiv, substitution) + val uniqueness = have(prem |- ∃!(u, f)) by Restate.from(just) + have(prem |- ∃!(u, completeDef)) by Cut(uniqueness, implication) + } + + val case2 = have(!prem |- ∃!(u, completeDef)) subproof { + val existence = have(!prem |- ∃(u, completeDef)) subproof { + have(!prem |- !prem) by Hypothesis + thenHave((prem, !prem) |- ()) by LeftNot + thenHave((prem, !prem) |- substF) by Weakening + val left = thenHave(!prem |- (prem ==> substF)) by Restate + + have(defaultValue === defaultValue) by RightRefl + thenHave(!prem |- defaultValue === defaultValue) by Weakening + val right = thenHave(!prem ==> (defaultValue === defaultValue)) by Restate + + have(!prem |- (prem ==> substF) /\ (!prem ==> (defaultValue === defaultValue))) by RightAnd(left, right) + thenHave(thesis) by RightExists.withParameters(defaultValue) + } + + val uniqueness = have((!prem, completeDef, substDef) |- (u === v)) subproof { + assume(!prem) + assume(completeDef) + assume(substDef) + + val eq1 = have(u === defaultValue) by Tautology + val eq2 = have(defaultValue === v) by Tautology + val p = have((u === defaultValue) /\ (defaultValue === v)) by RightAnd(eq1, eq2) + + val transitivity = Quantifiers.equalityTransitivity of (x -> u, y -> defaultValue, z -> v) + have(thesis) by Cut(p, transitivity) + } + + have(thesis) by ExistenceAndUniqueness(completeDef)(existence, uniqueness) + } + + have(thesis) by Tautology.from(case1, case2) + } + + The(u, completeDef)(completeUniquenessTheorem) + } + } + } + } diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala index 3439bad44..2ae17ea1a 100644 --- a/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala +++ b/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala @@ -917,16 +917,21 @@ object SetTheory extends lisa.Main { */ val setIntersection = DEF(x, y) --> The(z, ∀(t, in(t, z) <=> (in(t, x) /\ in(t, y))))(setIntersectionUniqueness) - val setIntersectionCommutativity = Theorem( - setIntersection(x, y) === setIntersection(y, x) + val setIntersectionMembership = Theorem( + in(t, setIntersection(x, y)) <=> (in(t, x) /\ in(t, y)) ) { - sorry + have(forall(t, in(t, setIntersection(x, y)) <=> (in(t, x) /\ in(t, y)))) by InstantiateForall(setIntersection(x, y))(setIntersection.definition) + thenHave(thesis) by InstantiateForall(t) } - val setIntersectionMembership = Theorem( - in(t, setIntersection(x, y)) <=> (in(t, x) /\ in(t, y)) + val setIntersectionCommutativity = Theorem( + setIntersection(x, y) === setIntersection(y, x) ) { - sorry + val left = have(in(t, setIntersection(x, y)) <=> (in(t, y) /\ in(t, x))) by Tautology.from(setIntersectionMembership) + val right = have(in(t, setIntersection(y, x)) <=> (in(t, y) /\ in(t, x))) by Tautology.from(setIntersectionMembership of (x := y, y := x)) + have(in(t, setIntersection(x, y)) <=> in(t, setIntersection(y, x))) by Tautology.from(left, right) + val equalityPrepare = thenHave(forall(t, (in(t, setIntersection(x, y)) <=> in(t, setIntersection(y, x))))) by RightForall + have(thesis) by Tautology.from(equalityPrepare, extensionalityAxiom of (x := setIntersection(x, y), y := setIntersection(y, x))) } extension (x: Term) { @@ -1030,6 +1035,11 @@ object SetTheory extends lisa.Main { */ val setDifference = DEF(x, y) --> The(z, ∀(t, in(t, z) <=> (in(t, x) /\ !in(t, y))))(setDifferenceUniqueness) + val setDifferenceMembership = Theorem(in(t, setDifference(x, y)) <=> (in(t, x) /\ !in(t, y))) { + have(∀(t, in(t, setDifference(x, y)) <=> (in(t, x) /\ !in(t, y)))) by InstantiateForall(setDifference(x, y))(setDifference.definition) + thenHave(thesis) by InstantiateForall(t) + } + /** * Theorem --- Intersection of a non-empty Class is a Set * diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheoryBasics.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheoryBasics.scala new file mode 100644 index 000000000..b95c498fd --- /dev/null +++ b/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheoryBasics.scala @@ -0,0 +1,270 @@ +package lisa.maths.settheory + +import lisa.automation.kernel.CommonTactics.Definition +import lisa.automation.settheory.SetTheoryTactics.* +import lisa.maths.Quantifiers.* +import lisa.maths.settheory.SetTheory.* +import lisa.maths.settheory.functions.Functionals.* + +import scala.collection.immutable.{Map => ScalaMap} +import lisa.maths.settheory.SetTheory.relationDomain + +object SetTheoryBasics extends lisa.Main { + + // var defs + private val x = variable + private val y = variable + private val z = variable + private val w = variable + private val a = variable + private val b = variable + private val c = variable + private val d = variable + private val t = variable + private val f = variable + private val r = variable + + /** + * Theorems about basic sets + */ + + /* + Theorem: Equality by Subset + x is equal to y iff x ⊆ y and y ⊆ x + */ + val equalityBySubset = Theorem((x === y) <=> (x ⊆ y /\ y ⊆ x)) { + val forward = have(x === y |- x ⊆ y /\ y ⊆ x) subproof { + assume(x === y) + have(forall(z, in(z, x) <=> in(z, y))) by Tautology.from(extensionalityAxiom) + val bothDirections = thenHave(in(z, x) <=> in(z, y)) by InstantiateForall(z) + thenHave(in(z, x) ==> in(z, y)) by Weakening + thenHave(forall(z, in(z, x) ==> in(z, y))) by RightForall + val leftSubset = have(x ⊆ y) by Tautology.from(lastStep, subsetAxiom) + have(in(z, y) ==> in(z, x)) by Weakening(bothDirections) + thenHave(forall(z, in(z, y) ==> in(z, x))) by RightForall + val rightSubset = have(y ⊆ x) by Tautology.from(lastStep, subsetAxiom of (x := y, y := x)) + have(thesis) by Tautology.from(leftSubset, rightSubset) + } + val backward = have((x ⊆ y /\ y ⊆ x) |- x === y) subproof { + assume((x ⊆ y), (y ⊆ x)) + have(forall(z, in(z, x) ==> in(z, y))) by Tautology.from(subsetAxiom) + val left = thenHave(in(z, x) ==> in(z, y)) by InstantiateForall(z) + have(forall(z, in(z, y) ==> in(z, x))) by Tautology.from(subsetAxiom of (x := y, y := x)) + val right = thenHave(in(z, y) ==> in(z, x)) by InstantiateForall(z) + have(in(z, x) <=> in(z, y)) by Tautology.from(left, right) + val equalityDef = thenHave(forall(z, in(z, x) <=> in(z, y))) by RightForall + have(thesis) by Tautology.from(equalityDef, extensionalityAxiom) + } + have(thesis) by Tautology.from(forward, backward) + } + + /* + Theorem: Equality replaces contains right side + if x is equal to y then we have z ∈ x iff z ∈ y for any z + */ + val replaceEqualityContainsRight = Theorem((x === y) ==> ((z ∈ x) <=> (z ∈ y))) { + have((x === y) |- ((z ∈ x) <=> (z ∈ y))) subproof { + assume(x === y) + have(forall(z, (z ∈ x) <=> (z ∈ y))) by Tautology.from(extensionalityAxiom) + thenHave(thesis) by InstantiateForall(z) + } + thenHave(thesis) by Tautology + } + + /* + Theorem: Equality replaces contains left side + if x is equal to y then we have x ∈ z iff y ∈ z for any z + */ + val replaceEqualityContainsLeft = Theorem((x === y) ==> ((x ∈ z) <=> (y ∈ z))) { + have(((x === y), (y ∈ z)) |- (x ∈ z)) subproof { + have((y ∈ z, (x === y)) |- (y ∈ z)) by Tautology + thenHave(thesis) by RightSubstEq.withParametersSimple(List((y, x)), lambda(x, in(x, z))) + } + have(thesis) by Tautology.from(lastStep, lastStep of (x := y, y := x)) + } + + /* + Theorem: Equality replaces subset right side + if x is equal to y then we have z ⊆ x iff z ⊆ y for any z + */ + val replaceEqualitySubsetRight = Theorem((x === y) ==> ((z ⊆ x) <=> (z ⊆ y))) { + val side = have(((x === y), (z ⊆ x)) |- (z ⊆ y)) subproof { + assume((x === y) /\ (z ⊆ x)) + have(thesis) by Tautology.from(equalityBySubset, subsetTransitivity of (a := z, b := x, c := y)) + } + have(thesis) by Tautology.from(side, side of (x := y, y := x)) + } + + /* + Theorem: Equality replaces subset left side + if x is equal to y then we have x ⊆ z iff y ⊆ z for any z + */ + val replaceEqualitySubsetLeft = Theorem((x === y) ==> ((x ⊆ z) <=> (y ⊆ z))) { + val side = have(((x === y), (x ⊆ z)) |- (y ⊆ z)) subproof { + assume((x === y) /\ (x ⊆ z)) + have(forall(w, in(w, x) ==> in(w, z))) by Tautology.from(subsetAxiom of (y := z, z := w)) + thenHave(in(w, x) ==> in(w, z)) by InstantiateForall(w) + have(in(w, y) ==> in(w, z)) by Tautology.from(lastStep, replaceEqualityContainsRight of (z := w)) + thenHave(forall(w, in(w, y) ==> in(w, z))) by RightForall + have(thesis) by Tautology.from(lastStep, subsetAxiom of (x := y, y := z)) + } + have(thesis) by Tautology.from(side, side of (x := y, y := x)) + } + + /* + Theorem: Subset is closed under intersection + if x ⊆ z and y ⊆ z we have x ∩ y ⊆ z + */ + val subsetClosedIntersection = Theorem((x ⊆ z, y ⊆ z) |- (x ∩ y) ⊆ z) { + assume(x ⊆ z, y ⊆ z) + have(forall(t, in(t, x) ==> in(t, z))) by Tautology.from(subsetAxiom of (y := z, z := t)) + val first = thenHave(in(t, x) ==> in(t, z)) by InstantiateForall(t) + + have(forall(t, in(t, y) ==> in(t, z))) by Tautology.from(subsetAxiom of (x := y, y := z, z := t)) + val second = thenHave(in(t, y) ==> in(t, z)) by InstantiateForall(t) + + have(in(t, setIntersection(x, y)) ==> in(t, z)) by Tautology.from(first, second, setIntersectionMembership) + thenHave(forall(t, in(t, setIntersection(x, y)) ==> in(t, z))) by RightForall + have(thesis) by Tautology.from(lastStep, subsetAxiom of (x := setIntersection(x, y), y := z)) + } + + /* + Theorem: Intersection means subset of both elements + if z ⊆ x ∩ y we know z ⊆ x and z ⊆ y + */ + val subsetUnderIntersection = Theorem((z ⊆ (x ∩ y)) |- (z ⊆ x /\ z ⊆ y)) { + assume(z ⊆ (x ∩ y)) + have(forall(t, in(t, z) ==> in(t, x ∩ y))) by Tautology.from(subsetAxiom of (x := z, y := x ∩ y, z := t)) + thenHave(in(t, z) ==> in(t, x ∩ y)) by InstantiateForall(t) + val both = have((in(t, z) ==> in(t, x)) /\ (in(t, z) ==> in(t, y))) by Tautology.from(lastStep, setIntersectionMembership of (x := x, y := y)) + have(in(t, z) ==> in(t, x)) by Weakening(both) + thenHave(forall(t, in(t, z) ==> in(t, x))) by RightForall + val first = have(z ⊆ x) by Tautology.from(lastStep, subsetAxiom of (x := z, y := x, z := t)) + have(in(t, z) ==> in(t, y)) by Weakening(both) + thenHave(forall(t, in(t, z) ==> in(t, y))) by RightForall + val second = have(z ⊆ y) by Tautology.from(lastStep, subsetAxiom of (x := z, y := y, z := t)) + have(thesis) by Tautology.from(first, second) + } + + /* + Theorem: Subset is closed under setUnion + if x ⊆ z and y ⊆ z we have x u y ⊆ z + */ + val subsetClosedSetUnion = Theorem((x ⊆ z, y ⊆ z) |- setUnion(x, y) ⊆ z) { + assume(x ⊆ z, y ⊆ z) + have(forall(t, in(t, x) ==> in(t, z))) by Tautology.from(subsetAxiom of (y := z, z := t)) + val first = thenHave(in(t, x) ==> in(t, z)) by InstantiateForall(t) + + have(forall(t, in(t, y) ==> in(t, z))) by Tautology.from(subsetAxiom of (x := y, y := z, z := t)) + val second = thenHave(in(t, y) ==> in(t, z)) by InstantiateForall(t) + + have(in(t, setUnion(x, y)) ==> in(t, z)) by Tautology.from(first, second, setUnionMembership of (z := t)) + thenHave(forall(t, in(t, setUnion(x, y)) ==> in(t, z))) by RightForall + have(thesis) by Tautology.from(lastStep, subsetAxiom of (x := setUnion(x, y), y := z)) + } + + /* + Theorem: Subset is closed under union + The union of any (finite or infinite) number of sets in y is still in y + if x ⊆ powerSet(y) we have union(x) ⊆ y + */ + val subsetClosedUnion = Theorem((x ⊆ powerSet(y)) |- union(x) ⊆ y) { + assume(x ⊆ powerSet(y)) + have(forall(z, in(z, x) ==> in(z, powerSet(y)))) by Tautology.from(subsetAxiom of (y := powerSet(y))) + thenHave(in(z, x) ==> in(z, powerSet(y))) by InstantiateForall(z) + have(in(z, x) |- forall(w, in(w, z) ==> in(w, y))) by Tautology.from(lastStep, powerAxiom of (x := z), subsetAxiom of (x := z, z := w)) + thenHave(in(z, x) |- (in(w, z) ==> in(w, y))) by InstantiateForall(w) + have((in(z, x) /\ in(w, z)) |- in(w, y)) by Tautology.from(lastStep) + thenHave(exists(z, in(z, x) /\ in(w, z)) |- in(w, y)) by LeftExists + have(in(w, union(x)) ==> in(w, y)) by Tautology.from(lastStep, unionAxiom of (z := w, y := z)) + thenHave(forall(w, in(w, union(x)) ==> in(w, y))) by RightForall + have(thesis) by Tautology.from(lastStep, subsetAxiom of (x := union(x))) + } + + /* + Theorem: Union doesnt shrink + The union of any (finite or infinite) number of sets where one set is x has to include x + if x ∈ y we have x ⊆ unnion(y) + */ + val unionDoesntShrink = Theorem((x ∈ y) |- (x ⊆ union(y))) { + assume(in(x, y)) + thenHave(in(z, x) |- (in(z, x) /\ in(x, y))) by Tautology + thenHave(in(z, x) |- exists(x, in(z, x) /\ in(x, y))) by RightExists + have(in(z, x) ==> in(z, union(y))) by Tautology.from(lastStep, unionAxiom of (x := y, y := x)) + thenHave(forall(z, in(z, x) ==> in(z, union(y)))) by RightForall + have(thesis) by Tautology.from(lastStep, subsetAxiom of (x := x, y := union(y))) + } + + /* + Theorem: Subset propagates over elementOf + if z ∈ x and x ⊆ y we have z ∈ y + */ + val subsetTactic = Theorem((x ⊆ y, z ∈ x) |- z ∈ y) { + assume(x ⊆ y, z ∈ x) + + have(forall(z, z ∈ x ==> z ∈ y)) by Tautology.from(subsetAxiom) + thenHave(z ∈ x ==> z ∈ y) by InstantiateForall(z) + thenHave(thesis) by Tautology + } + + /* + Theorem: Difference shrinks + x \ y ⊆ x + */ + val differenceShrinks = Theorem(setDifference(x, y) ⊆ x) { + have(in(z, setDifference(x, y)) ==> in(z, x)) by Tautology.from(setDifferenceMembership of (t := z)) + thenHave(forall(z, in(z, setDifference(x, y)) ==> in(z, x))) by RightForall + have(thesis) by Tautology.from(lastStep, subsetAxiom of (x := setDifference(x, y), y := x)) + } + + /** + * Lemma --- Range introduction and elimination rules. If en element is in the image of a function, then it has a preimage inside its domain. + * + * `functional(f) |- y ⊆ Im(f) <=> ∃x ∈ Dom(f). f(x) = y` + */ + val functionRangeMembership = Lemma(functional(f) |- in(y, relationRange(f)) <=> ∃(x, in(x, relationDomain(f)) /\ (app(f, x) === y))) { + assume(functional(f)) + + have(forall(y, y ∈ relationRange(f) <=> ∃(x, in(pair(x, y), f)))) by InstantiateForall(relationRange(f))(relationRange.definition of (r := f)) + val defRange = thenHave(y ∈ relationRange(f) <=> ∃(x, in(pair(x, y), f))) by InstantiateForall(y) + + have(∀(x, x ∈ relationDomain(f) <=> ∃(y, pair(x, y) ∈ f))) by InstantiateForall(relationDomain(f))(relationDomain.definition of (r := f)) + val defDomain = thenHave(x ∈ relationDomain(f) <=> ∃(y, pair(x, y) ∈ f)) by InstantiateForall(x) + + val forward = have(y ∈ relationRange(f) ==> ∃(x, in(x, relationDomain(f)) /\ (app(f, x) === y))) subproof { + assume(y ∈ relationRange(f)) + have(pair(x, y) ∈ f |- pair(x, y) ∈ f) by Tautology + thenHave(pair(x, y) ∈ f |- ∃(y, pair(x, y) ∈ f)) by RightExists + have(pair(x, y) ∈ f |- x ∈ relationDomain(f) /\ (app(f, x) === y)) by Tautology.from( + lastStep, + pairInFunctionIsApp of (a := x, b := y), + defDomain + ) + thenHave(in(pair(x, y), f) |- ∃(x, x ∈ relationDomain(f) /\ (app(f, x) === y))) by RightExists + thenHave(∃(x, in(pair(x, y), f)) |- ∃(x, x ∈ relationDomain(f) /\ (app(f, x) === y))) by LeftExists + have(thesis) by Tautology.from(lastStep, defRange) + } + + val backward = have(∃(x, in(x, relationDomain(f)) /\ (app(f, x) === y)) |- y ∈ relationRange(f)) subproof { + have(in(x, relationDomain(f)) /\ (app(f, x) === y) |- pair(x, y) ∈ f) by Tautology.from(pairInFunctionIsApp of (a := x, b := y)) + thenHave(in(x, relationDomain(f)) /\ (app(f, x) === y) |- ∃(x, pair(x, y) ∈ f)) by RightExists + have(in(x, relationDomain(f)) /\ (app(f, x) === y) |- y ∈ relationRange(f)) by Tautology.from( + lastStep, + defRange + ) + thenHave(thesis) by LeftExists + } + + have(thesis) by Tautology.from(forward, backward) + } + + val equalitySymmetry = Theorem( + x === y |- y === x + ) { + have(thesis) by Tautology.from(equalityBySubset, equalityBySubset of (x := y, y := x)) + } + + val equalityReflexivity = Theorem(x === x) { + have(thesis) by Tautology.from(equalityBySubset of (x := x, y := x)) + } +} diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/functions/DirectPreimages.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/functions/DirectPreimages.scala new file mode 100644 index 000000000..9e9633470 --- /dev/null +++ b/lisa-sets/src/main/scala/lisa/maths/settheory/functions/DirectPreimages.scala @@ -0,0 +1,857 @@ +package lisa.maths.settheory.functions + +import lisa.automation.kernel.CommonTactics.Definition +import lisa.automation.settheory.SetTheoryTactics.* +import lisa.maths.Quantifiers.* +import lisa.maths.settheory.SetTheoryBasics.* +import lisa.automation.kernel.CommonTactics.* +import lisa.maths.settheory.functions.Functionals.* +import lisa.automation.settheory.SetTheoryTactics.UniqueComprehension +import lisa.automation.settheory.SetTheoryTactics.TheConditional +import lisa.maths.settheory.SetTheory.* +import javax.swing.text.html.HTML.Tag + +object DirectPreimages extends lisa.Main { + + // var defs + private val x, y, z, a, b, c, t, p, f, r, s = variable + private val X, T, T1, T2 = variable + private val S, A, B, Y, o, O, O2, O3 = variable + + /** + * Don't know why, but I need to paste it directly here otherwise we have a matcherror null error (from FunctionProperties) + */ + val surjective = DEF(f, x, y) --> functionFrom(f, x, y) /\ ∀(b, in(b, y) ==> ∃(a, in(pair(a, b), f))) + + /* Also copied the theorem (from FunctionProperties) */ + val surjectiveImpliesRangeIsCodomain = Theorem( + surjective(f, x, y) |- (y === functionRange(f)) + ) { + have(surjective(f, x, y) |- ∀(b, in(b, y) ==> ∃(a, in(pair(a, b), f)))) by Tautology.from(surjective.definition) + val surjDef = thenHave(surjective(f, x, y) |- in(b, y) ==> ∃(a, in(pair(a, b), f))) by InstantiateForall(b) + have(∀(t, in(t, functionRange(f)) <=> (∃(a, in(pair(a, t), f))))) by InstantiateForall(functionRange(f))(functionRange.definition of (r -> f)) + val rangeDef = thenHave(in(b, functionRange(f)) <=> (∃(a, in(pair(a, b), f)))) by InstantiateForall(b) + + have(surjective(f, x, y) |- in(b, y) ==> in(b, functionRange(f))) by Tautology.from(surjDef, rangeDef) + thenHave(surjective(f, x, y) |- ∀(b, in(b, y) ==> in(b, functionRange(f)))) by RightForall + val surjsub = andThen(Substitution.applySubst(subsetAxiom of (x -> y, y -> functionRange(f)))) + + have((surjective(f, x, y), functionFrom(f, x, y)) |- subset(y, functionRange(f)) /\ subset(functionRange(f), y)) by RightAnd(surjsub, functionImpliesRangeSubsetOfCodomain) + val funceq = andThen(Substitution.applySubst(subsetEqualitySymmetry of (x -> y, y -> functionRange(f)))) + + val surjfunc = have(surjective(f, x, y) |- functionFrom(f, x, y)) by Tautology.from(surjective.definition) + + have(thesis) by Cut(surjfunc, funceq) + } + + // The formula for direct image that will be used throughout the definitions and theorems of uniqueness + inline def directImageFormula = y ∈ s <=> (y ∈ Y /\ ∃(x, (app(f, x) === y) /\ x ∈ A)) + + // This direct image is unique + val directImageUniqueness = Theorem( + (functionFrom(f, X, Y), subset(A, X)) |- ∃!(s, ∀(y, directImageFormula)) + ) { + have(∃!(s, ∀(y, directImageFormula))) by UniqueComprehension(Y, lambda(y, ∃(x, (app(f, x) === y) /\ x ∈ A))) + thenHave(thesis) by Weakening + } + + /** + * Direct image by a function + * f(A) = { y ∈ Y | ∃x ∈ A, f(x) = y } + */ + val directImage = DEF(f, X, Y, A) --> TheConditional(s, ∀(y, directImageFormula))(directImageUniqueness) + + /* + * Useful statement about membership in the direct image + */ + val directImageMembership = Theorem((functionFrom(f, X, Y), subset(A, X)) |- y ∈ directImage(f, X, Y, A) <=> (y ∈ Y /\ ∃(x, (app(f, x) === y) /\ x ∈ A))) { + assume(functionFrom(f, X, Y) /\ subset(A, X)) + have(∀(z, z ∈ directImage(f, X, Y, A) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ A)))) by InstantiateForall(directImage(f, X, Y, A))(directImage.definition) + thenHave(thesis) by InstantiateForall(y) + } + + /** + * Theorem + * f(A ∪ B) = f(A) ∪ f(B) + */ + val directImageSetUnion = Theorem( + functionFrom(f, X, Y) /\ + subset(A, X) /\ + subset(B, X) + |- setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B)) === directImage(f, X, Y, setUnion(A, B)) + ) { + assume( + functionFrom(f, X, Y) /\ + subset(A, X) /\ + subset(B, X) + ) + + val subsetAorB = have(subset(setUnion(A, B), X)) by Tautology.from(unionOfTwoSubsets of (a := A, b := B, c := X)) + + have(∀(z, z ∈ directImage(f, X, Y, A) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ A)))) by InstantiateForall(directImage(f, X, Y, A))(directImage.definition) + val defA = thenHave(z ∈ directImage(f, X, Y, A) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ A))) by InstantiateForall(z) + have(∀(z, z ∈ directImage(f, X, Y, B) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ B)))) by InstantiateForall(directImage(f, X, Y, B))(directImage.definition of (A := B)) + val defB = thenHave(z ∈ directImage(f, X, Y, B) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ B))) by InstantiateForall(z) + have( + subset(setUnion(A, B), X) |- + ∀( + z, + z ∈ directImage(f, X, Y, setUnion(A, B)) <=> + (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ setUnion(A, B))) + ) + ) by InstantiateForall(directImage(f, X, Y, setUnion(A, B)))(directImage.definition of (A := setUnion(A, B))) + thenHave( + subset(setUnion(A, B), X) |- + z ∈ directImage(f, X, Y, setUnion(A, B)) <=> + (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ setUnion(A, B))) + ) by InstantiateForall(z) + val defAorB = have( + z ∈ directImage(f, X, Y, setUnion(A, B)) <=> + (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ setUnion(A, B))) + ) by Tautology.from(lastStep, subsetAorB) + + val forward = have(z ∈ setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B)) ==> z ∈ directImage(f, X, Y, setUnion(A, B))) subproof { + val firstPart = have(z ∈ setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B)) |- (z ∈ directImage(f, X, Y, A)) \/ (z ∈ directImage(f, X, Y, B))) by Tautology.from( + setUnionMembership of (x := directImage(f, X, Y, A), y := directImage(f, X, Y, B)) + ) + assume(z ∈ setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B))) + have(z ∈ Y /\ ((∃(x, (app(f, x) === z) /\ x ∈ A)) \/ ∃(x, (app(f, x) === z) /\ x ∈ B))) by Tautology.from( + defA, + defB, + firstPart + ) + val partialResult = thenHave(z ∈ Y /\ (∃(x, (app(f, x) === z) /\ ((x ∈ A) \/ (x ∈ B))))) by Tautology + have( + (z ∈ Y, (app(f, x) === z) /\ ((x ∈ A) \/ (x ∈ B))) + |- + (app(f, x) === z) /\ x ∈ setUnion(A, B) + ) by Tautology.from(setUnionMembership of (x := A, y := B, z := x), defAorB) + thenHave((z ∈ Y, (app(f, x) === z) /\ ((x ∈ A) \/ (x ∈ B))) |- ∃(x, (app(f, x) === z) /\ x ∈ setUnion(A, B))) by RightExists + have((z ∈ Y, (app(f, x) === z) /\ ((x ∈ A) \/ (x ∈ B))) |- z ∈ directImage(f, X, Y, setUnion(A, B))) by Tautology.from(lastStep, defAorB) + thenHave((z ∈ Y, ∃(x, (app(f, x) === z) /\ ((x ∈ A) \/ (x ∈ B)))) |- z ∈ directImage(f, X, Y, setUnion(A, B))) by LeftExists + have(z ∈ directImage(f, X, Y, setUnion(A, B))) by Tautology.from(lastStep, partialResult) + } + val backward = have(z ∈ directImage(f, X, Y, setUnion(A, B)) ==> z ∈ setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B))) subproof { + val intermediate = have( + z ∈ Y /\ (app(f, x) === z) /\ x ∈ setUnion(A, B) |- + (z ∈ Y /\ (app(f, x) === z) /\ x ∈ A) + \/ (z ∈ Y /\ (app(f, x) === z) /\ x ∈ B) + ) by Tautology.from(setUnionMembership of (x := A, y := B, z := x)) + + assume(z ∈ directImage(f, X, Y, setUnion(A, B))) + have(z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ setUnion(A, B))) by Tautology.from(defAorB) + have((app(f, x) === z) /\ x ∈ A |- (app(f, x) === z) /\ x ∈ A) by Tautology + val existsA = thenHave( + (app(f, x) === z) /\ x ∈ A |- + ∃(x, (app(f, x) === z) /\ x ∈ A) + ) by RightExists + have((app(f, x) === z) /\ x ∈ B |- (app(f, x) === z) /\ x ∈ B) by Tautology + val existsB = thenHave( + (app(f, x) === z) /\ x ∈ B |- + ∃(x, (app(f, x) === z) /\ x ∈ B) + ) by RightExists + have( + z ∈ Y /\ (app(f, x) === z) /\ x ∈ setUnion(A, B) |- + (z ∈ directImage(f, X, Y, A)) \/ (z ∈ directImage(f, X, Y, B)) + ) by Tautology.from(intermediate, existsA, existsB, defA, defB) + have( + (z ∈ Y, (app(f, x) === z) /\ x ∈ setUnion(A, B)) |- + z ∈ setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B)) + ) by Tautology.from(lastStep, setUnionMembership of (x := directImage(f, X, Y, A), y := directImage(f, X, Y, B), z := z)) + thenHave( + (z ∈ Y, ∃(x, (app(f, x) === z) /\ x ∈ setUnion(A, B))) |- + z ∈ setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B)) + ) by LeftExists + have(z ∈ setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B))) by Tautology.from(lastStep, defAorB) + } + have(z ∈ directImage(f, X, Y, setUnion(A, B)) <=> z ∈ setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B))) by RightIff(forward, backward) + thenHave(∀(z, z ∈ directImage(f, X, Y, setUnion(A, B)) <=> z ∈ setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B)))) by RightForall + andThen(Substitution.applySubst(extensionalityAxiom of (x := directImage(f, X, Y, setUnion(A, B)), y := setUnion(directImage(f, X, Y, A), directImage(f, X, Y, B))))) + } + + /** + * Theorem -- direct image of the empty set + * f(∅) = ∅ + */ + val directImageEmptySet = Theorem( + (functionFrom(f, X, Y)) + |- directImage(f, X, Y, emptySet) === emptySet + ) { + assume(functionFrom(f, X, Y)) + + have(subset(emptySet, X) |- ∀(z, z ∈ directImage(f, X, Y, emptySet) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ emptySet)))) by InstantiateForall(directImage(f, X, Y, emptySet))( + directImage.definition of (A := emptySet) + ) + thenHave(subset(emptySet, X) |- y ∈ directImage(f, X, Y, emptySet) <=> (y ∈ Y /\ ∃(x, (app(f, x) === y) /\ x ∈ emptySet))) by InstantiateForall(y) + val defA = have(y ∈ directImage(f, X, Y, emptySet) <=> (y ∈ Y /\ ∃(x, (app(f, x) === y) /\ x ∈ emptySet))) by Tautology.from(lastStep, emptySetIsASubset of (x := X)) + + val noElements = have(!in(y, directImage(f, X, Y, emptySet))) subproof { + assume(in(y, directImage(f, X, Y, emptySet))) + have((app(f, x) === y) /\ x ∈ emptySet |- x ∈ emptySet) by Tautology + have((app(f, x) === y) /\ x ∈ emptySet |- False) by Tautology.from(lastStep, emptySetAxiom) + thenHave(∃(x, (app(f, x) === y) /\ x ∈ emptySet) |- False) by LeftExists + have(False) by Tautology.from(lastStep, defA) + } + thenHave(∀(y, !in(y, directImage(f, X, Y, emptySet)))) by RightForall + + have(thesis) by Tautology.from(lastStep, setWithNoElementsIsEmpty of (x := directImage(f, X, Y, emptySet))) + } + + /** + * Theorem -- the direct image is always in the codomain + * f(A) ⊆ f(X) + */ + val directImageSubsetCodomain = Theorem( + (functionFrom(f, X, Y), subset(A, X)) + |- directImage(f, X, Y, A) ⊆ functionRange(f) + ) { + assume(functionFrom(f, X, Y), subset(A, X)) + + have(∀(y, y ∈ relationRange(f) <=> ∃(x, in(pair(x, y), f)))) by InstantiateForall(relationRange(f))(relationRange.definition of (r := f)) + val defRange = thenHave(z ∈ relationRange(f) <=> ∃(x, in(pair(x, z), f))) by InstantiateForall(z) + + have(∀(z, z ∈ directImage(f, X, Y, A) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ A)))) by InstantiateForall(directImage(f, X, Y, A))(directImage.definition) + val defA = thenHave(z ∈ directImage(f, X, Y, A) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ A))) by InstantiateForall(z) + + have(z ∈ directImage(f, X, Y, A) ==> z ∈ functionRange(f)) subproof { + assume(z ∈ directImage(f, X, Y, A)) + have(∃(x, (app(f, x) === z) /\ x ∈ A)) by Tautology.from(defA) + have(x ∈ A /\ (app(f, x) === z) |- pair(x, z) ∈ f) by Tautology.from( + pairInFunctionIsApp of (a := x, b := z), + functionFromImpliesFunctional of (x := X, y := Y), + subsetTactic of (x := A, y := X, z := x), + functionFromImpliesDomainEq of (x := X, y := Y), + replaceEqualityContainsRight of (x := functionDomain(f), y := X, z := x) + ) + thenHave(x ∈ A /\ (app(f, x) === z) |- ∃(x, pair(x, z) ∈ f)) by RightExists + have(x ∈ A /\ (app(f, x) === z) |- z ∈ relationRange(f)) by Tautology.from(lastStep, defRange) + thenHave(∃(x, x ∈ A /\ (app(f, x) === z)) |- z ∈ relationRange(f)) by LeftExists + have(∃(x, x ∈ A /\ (app(f, x) === z)) |- z ∈ relationRange(f) /\ z ∈ Y) by Tautology.from( + lastStep, + functionImpliesRangeSubsetOfCodomain of (x := X, y := Y), + subsetTactic of (x := relationRange(f), y := Y) + ) + have(thesis) by Tautology.from(lastStep, defA) + } + + thenHave(∀(z, z ∈ directImage(f, X, Y, A) ==> z ∈ functionRange(f))) by RightForall + have(thesis) by Tautology.from(subsetAxiom of (x := directImage(f, X, Y, A), y := functionRange(f)), lastStep) + } + + /** + * Theorem -- congruence/substitution property for the direct image + * + * Needed as a lemma for other proofs + */ + val applyDirectImage = Theorem( + A === B |- directImage(f, X, Y, A) === directImage(f, X, Y, B) + ) { + have(((A === B), in(z, directImage(f, X, Y, A))) |- in(z, directImage(f, X, Y, B))) subproof { + have(((A === B), in(z, directImage(f, X, Y, A))) |- in(z, directImage(f, X, Y, A))) by Tautology + thenHave(thesis) by RightSubstEq.withParametersSimple(List((A, B)), lambda(x, in(z, directImage(f, X, Y, x)))) + } + have(A === B |- in(z, directImage(f, X, Y, A)) <=> in(z, directImage(f, X, Y, B))) by Tautology.from(lastStep, lastStep of (A := B, B := A)) + thenHave(A === B |- ∀(z, in(z, directImage(f, X, Y, A)) <=> in(z, directImage(f, X, Y, B)))) by RightForall + have(thesis) by Tautology.from(lastStep, extensionalityAxiom of (x := directImage(f, X, Y, A), y := directImage(f, X, Y, B))) + } + + /** + * Theorem -- the direct image is monotonic + * + * If A ⊆ B then f(A) ⊆ f(B) + */ + val directImageMonotonicity = Theorem( + (functionFrom(f, X, Y), A ⊆ B, B ⊆ X) |- directImage(f, X, Y, A) ⊆ directImage(f, X, Y, B) + ) { + assume(functionFrom(f, X, Y), A ⊆ B, B ⊆ X) + + val aSubsetOfX = have(A ⊆ X) by Tautology.from(subsetTransitivity of (a := A, b := B, c := X)) + + have((app(f, x) === z) /\ x ∈ A |- (app(f, x) === z) /\ x ∈ B) by Tautology.from(subsetTactic of (x := A, y := B, z := x)) + thenHave((app(f, x) === z) /\ x ∈ A |- ∃(x, (app(f, x) === z) /\ x ∈ B)) by RightExists + thenHave(∃(x, (app(f, x) === z) /\ x ∈ A) |- ∃(x, (app(f, x) === z) /\ x ∈ B)) by LeftExists + have(z ∈ directImage(f, X, Y, A) |- z ∈ directImage(f, X, Y, B)) by Tautology.from( + lastStep, + aSubsetOfX, + directImageMembership of (y := z), + directImageMembership of (y := z, A := B) + ) + + thenHave(z ∈ directImage(f, X, Y, A) ==> z ∈ directImage(f, X, Y, B)) by Tautology + thenHave(∀(z, z ∈ directImage(f, X, Y, A) ==> z ∈ directImage(f, X, Y, B))) by RightForall + have(thesis) by Tautology.from(lastStep, subsetAxiom of (x := directImage(f, X, Y, A), y := directImage(f, X, Y, B))) + } + + inline def preimageFormula = x ∈ s <=> (x ∈ X /\ app(f, x) ∈ B) + + val preimageUniqueness = Theorem( + (functionFrom(f, X, Y), subset(B, Y)) |- ∃!(s, ∀(x, preimageFormula)) + ) { + have(∃!(s, ∀(x, preimageFormula))) by UniqueComprehension(X, lambda(x, app(f, x) ∈ B)) + thenHave(thesis) by Weakening + } + + /** + * Preimage by a function + * f^(-1)(B) = { x ∈ X | f(x) ∈ B } + */ + val preimage = DEF(f, X, Y, B) --> TheConditional(s, ∀(x, preimageFormula))(preimageUniqueness) + + /** + * Useful statement about membership in the preimage + */ + val preimageMembership = Theorem((functionFrom(f, X, Y), subset(B, Y)) |- x ∈ preimage(f, X, Y, B) <=> (x ∈ X /\ app(f, x) ∈ B)) { + assume(functionFrom(f, X, Y) /\ subset(B, Y)) + have(∀(x, x ∈ preimage(f, X, Y, B) <=> (x ∈ X /\ app(f, x) ∈ B))) by InstantiateForall(preimage(f, X, Y, B))(preimage.definition) + thenHave(thesis) by InstantiateForall(x) + } + + /** + * Theorem -- the preimage is always in the domain + * f^(-1)(A) ⊆ X + */ + val preimageSubset = Theorem( + (functionFrom(f, X, Y), subset(A, Y)) |- preimage(f, X, Y, A) ⊆ X + ) { + assume(functionFrom(f, X, Y) /\ subset(A, Y)) + have(in(z, preimage(f, X, Y, A)) ==> in(z, X)) by Tautology.from(preimageMembership of (B := A, x := z)) + thenHave(∀(z, in(z, preimage(f, X, Y, A)) ==> in(z, X))) by RightForall + have(thesis) by Tautology.from(lastStep, subsetAxiom of (x := preimage(f, X, Y, A), y := X)) + } + + /** + * Theorem -- the preimage of the codomain is the domain + * f^(-1)(Y) = X + */ + val preimageY = Theorem( + functionFrom(f, X, Y) |- preimage(f, X, Y, Y) === X + ) { + assume(functionFrom(f, X, Y)) + val first = have(preimage(f, X, Y, Y) ⊆ X) by Tautology.from(subsetReflexivity of (x := Y), preimageSubset of (A := Y)) + + have(in(z, X) ==> in(z, preimage(f, X, Y, Y))) by Tautology.from( + functionFromApplication of (x := X, y := Y, a := z), + functionFrom.definition of (x := X, y := Y), + preimageMembership of (x := z, B := Y), + subsetReflexivity of (x := Y) + ) + thenHave(∀(z, in(z, X) ==> in(z, preimage(f, X, Y, Y)))) by RightForall + val second = have(X ⊆ preimage(f, X, Y, Y)) by Tautology.from(lastStep, subsetAxiom of (x := X, y := preimage(f, X, Y, Y))) + have(thesis) by Tautology.from(first, second, equalityBySubset of (x := X, y := preimage(f, X, Y, Y))) + } + + /** + * Theorem -- the preimage of the union is the union of the preimages (case with only two subsets) + * f^(-1)(A ∪ B) = f^(-1)(A) ∪ f^(-1)(B) + */ + val preimageSetUnion = Theorem( + functionFrom(f, X, Y) /\ + subset(A, Y) /\ + subset(B, Y) + |- setUnion(preimage(f, X, Y, A), preimage(f, X, Y, B)) === preimage(f, X, Y, setUnion(A, B)) + ) { + assume( + functionFrom(f, X, Y) /\ + subset(A, Y) /\ + subset(B, Y) + ) + + val subsetAorB = have(subset(setUnion(A, B), Y)) by Tautology.from(unionOfTwoSubsets of (a := A, b := B, c := Y)) + + have(∀(z, z ∈ preimage(f, X, Y, A) <=> (z ∈ X /\ app(f, z) ∈ A))) by InstantiateForall(preimage(f, X, Y, A))(preimage.definition of (B := A)) + val defA = thenHave(z ∈ preimage(f, X, Y, A) <=> (z ∈ X /\ app(f, z) ∈ A)) by InstantiateForall(z) + have(∀(z, z ∈ preimage(f, X, Y, B) <=> (z ∈ X /\ app(f, z) ∈ B))) by InstantiateForall(preimage(f, X, Y, B))(preimage.definition) + val defB = thenHave(z ∈ preimage(f, X, Y, B) <=> (z ∈ X /\ app(f, z) ∈ B)) by InstantiateForall(z) + have( + subset(setUnion(A, B), Y) |- + ∀( + z, + z ∈ preimage(f, X, Y, setUnion(A, B)) <=> + (z ∈ X /\ app(f, z) ∈ setUnion(A, B)) + ) + ) by InstantiateForall(preimage(f, X, Y, setUnion(A, B)))(preimage.definition of (B := setUnion(A, B))) + thenHave( + subset(setUnion(A, B), Y) |- + z ∈ preimage(f, X, Y, setUnion(A, B)) <=> (z ∈ X /\ app(f, z) ∈ setUnion(A, B)) + ) by InstantiateForall(z) + val defAorB = have( + z ∈ preimage(f, X, Y, setUnion(A, B)) <=> (z ∈ X /\ app(f, z) ∈ setUnion(A, B)) + ) by Tautology.from(lastStep, subsetAorB) + + val forward = have(z ∈ setUnion(preimage(f, X, Y, A), preimage(f, X, Y, B)) ==> z ∈ preimage(f, X, Y, setUnion(A, B))) subproof { + val firstPart = have(z ∈ setUnion(preimage(f, X, Y, A), preimage(f, X, Y, B)) |- (z ∈ preimage(f, X, Y, A)) \/ (z ∈ preimage(f, X, Y, B))) by Tautology.from( + setUnionMembership of (x := preimage(f, X, Y, A), y := preimage(f, X, Y, B)) + ) + assume(z ∈ setUnion(preimage(f, X, Y, A), preimage(f, X, Y, B))) + have(z ∈ X /\ ((app(f, z) ∈ A) \/ (app(f, z) ∈ B))) by Tautology.from( + defA, + defB, + firstPart + ) + val partialResult = have(z ∈ X /\ (app(f, z) ∈ setUnion(A, B))) by Tautology.from( + lastStep, + setUnionMembership of (x := A, y := B, z := app(f, z)) + ) + have(thesis) by Tautology.from(defAorB, lastStep) + } + val backward = have(z ∈ preimage(f, X, Y, setUnion(A, B)) ==> z ∈ setUnion(preimage(f, X, Y, A), preimage(f, X, Y, B))) subproof { + assume(z ∈ preimage(f, X, Y, setUnion(A, B))) + have((z ∈ preimage(f, X, Y, A)) \/ (z ∈ preimage(f, X, Y, B))) by Tautology.from( + defAorB, + setUnionMembership of (x := A, y := B, z := app(f, z)), + defA, + defB + ) + have(thesis) by Tautology.from( + lastStep, + setUnionMembership of (x := preimage(f, X, Y, A), y := preimage(f, X, Y, B), z := z) + ) + } + have(z ∈ preimage(f, X, Y, setUnion(A, B)) <=> z ∈ setUnion(preimage(f, X, Y, A), preimage(f, X, Y, B))) by RightIff(forward, backward) + thenHave(∀(z, z ∈ preimage(f, X, Y, setUnion(A, B)) <=> z ∈ setUnion(preimage(f, X, Y, A), preimage(f, X, Y, B)))) by RightForall + andThen(Substitution.applySubst(extensionalityAxiom of (x := preimage(f, X, Y, setUnion(A, B)), y := setUnion(preimage(f, X, Y, A), preimage(f, X, Y, B))))) + } + + /** + * Theorem -- the complement of the preimage is the preimage of the complement + * X \ f^(-1)(A) = f^(-1)(Y \ A) + */ + val preimageDifference = Theorem( + (functionFrom(f, X, Y), subset(A, Y)) + |- setDifference(X, preimage(f, X, Y, A)) === preimage(f, X, Y, setDifference(Y, A)) + ) { + assume(functionFrom(f, X, Y), subset(A, Y)) + + have(∀(t, t ∈ setDifference(Y, A) <=> (in(t, Y) /\ !in(t, A)))) by InstantiateForall(setDifference(Y, A))(setDifference.definition of (x := Y, y := A)) + val defDiffY = thenHave(z ∈ setDifference(Y, A) <=> (in(z, Y) /\ !in(z, A))) by InstantiateForall(z) + + val forward = have(x ∈ setDifference(X, preimage(f, X, Y, A)) ==> x ∈ preimage(f, X, Y, setDifference(Y, A))) subproof { + assume(x ∈ setDifference(X, preimage(f, X, Y, A))) + + have(in(x, X) /\ !in(x, preimage(f, X, Y, A))) by Tautology.from(setDifferenceMembership of (t := x, x := X, y := preimage(f, X, Y, A))) + have(in(x, X) /\ !in(app(f, x), A)) by Tautology.from(lastStep, preimageMembership of (B := A)) + // (x ∈ X /\ app(f, x) ∈ setDifference(Y, A)) + have(in(x, X) /\ in(app(f, x), setDifference(Y, A))) by Tautology.from( + lastStep, + functionFromApplication of (x := X, y := Y, a := x), + functionFrom.definition of (x := X, y := Y), + setDifferenceMembership of (t := app(f, x), x := Y, y := A) + ) + have(thesis) by Tautology.from(lastStep, differenceShrinks of (x := Y, y := A), preimageMembership of (B := setDifference(Y, A))) + } + + val backward = have(x ∈ preimage(f, X, Y, setDifference(Y, A)) ==> x ∈ setDifference(X, preimage(f, X, Y, A))) subproof { + assume(x ∈ preimage(f, X, Y, setDifference(Y, A))) + have(x ∈ X /\ app(f, x) ∈ Y /\ !(app(f, x) ∈ A)) by Tautology.from( + preimageMembership of (B := setDifference(Y, A)), + setDifferenceMembership of (t := app(f, x), x := Y, y := A), + differenceShrinks of (x := Y, y := A) + ) + have(thesis) by Tautology.from(lastStep, preimageMembership of (B := A, t := x), setDifferenceMembership of (t := x, x := X, y := preimage(f, X, Y, A))) + } + + have(x ∈ setDifference(X, preimage(f, X, Y, A)) <=> x ∈ preimage(f, X, Y, setDifference(Y, A))) by RightIff(forward, backward) + thenHave(∀(x, x ∈ setDifference(X, preimage(f, X, Y, A)) <=> x ∈ preimage(f, X, Y, setDifference(Y, A)))) by RightForall + andThen(Substitution.applySubst(extensionalityAxiom of (x := setDifference(X, preimage(f, X, Y, A)), y := preimage(f, X, Y, setDifference(Y, A))))) + } + + /** + * ************** + * Set of preimages of a set of subsets + * Useful for the lemma about the preimage of the union + * *************** + */ + inline def preimagesFormula = x ∈ s <=> (x ∈ powerSet(X) /\ ∃(a, a ∈ A /\ (x === preimage(f, X, Y, a)))) + + val preimagesUniqueness = Theorem( + (functionFrom(f, X, Y), A ⊆ powerSet(Y)) |- ∃!(s, ∀(x, preimagesFormula)) + ) { + have(∃!(s, ∀(x, preimagesFormula))) by UniqueComprehension(powerSet(X), lambda(x, ∃(a, a ∈ A /\ (x === preimage(f, X, Y, a))))) + thenHave(thesis) by Weakening + } + + /** + * Set of preimages of a set of subsets + * { f^(-1)(A_i) | A_i ∈ A } + */ + val preimages = DEF(f, X, Y, A) --> TheConditional(s, ∀(x, preimagesFormula))(preimagesUniqueness) + + /** + * Useful statement about membership in the preimages + */ + val preimagesMembership = Theorem((functionFrom(f, X, Y), A ⊆ powerSet(Y)) |- x ∈ preimages(f, X, Y, A) <=> (x ∈ powerSet(X) /\ ∃(a, a ∈ A /\ (x === preimage(f, X, Y, a))))) { + assume(functionFrom(f, X, Y) /\ A ⊆ powerSet(Y)) + have(∀(x, x ∈ preimages(f, X, Y, A) <=> (x ∈ powerSet(X) /\ ∃(a, a ∈ A /\ (x === preimage(f, X, Y, a)))))) by InstantiateForall(preimages(f, X, Y, A))(preimages.definition) + thenHave(thesis) by InstantiateForall(x) + } + + /** + * Theorem -- generalization of `preimageSetUnion` + * The preimage of an arbitrary union is the union of preimages + * f^(-1)(⋃B) = ⋃(f^(-1)(B)) + * + * This is why we needed the definition of `preimages`! + */ + val preimageUnionThm = Theorem( + (functionFrom(f, X, Y), B ⊆ powerSet(Y)) |- + preimage(f, X, Y, union(B)) === union(preimages(f, X, Y, B)) + ) { + assume(functionFrom(f, X, Y), B ⊆ powerSet(Y)) + + val forward = have(x ∈ preimage(f, X, Y, union(B)) ==> x ∈ union(preimages(f, X, Y, B))) subproof { + assume(x ∈ preimage(f, X, Y, union(B))) + + val yInY = have(x ∈ X /\ app(f, x) ∈ y /\ y ∈ B |- y ⊆ Y) by Tautology.from( + subsetTactic of (x := B, y := powerSet(Y), z := y), + powerAxiom of (x := y, y := Y) + ) + + have(x ∈ X /\ app(f, x) ∈ y /\ y ∈ B |- y ∈ B /\ (preimage(f, X, Y, y) === preimage(f, X, Y, y))) by Tautology.from( + lastStep, + equalityReflexivity of (x := preimage(f, X, Y, y)) + ) + thenHave(x ∈ X /\ app(f, x) ∈ y /\ y ∈ B |- ∃(a, a ∈ B /\ (preimage(f, X, Y, y) === preimage(f, X, Y, a)))) by RightExists + have(x ∈ X /\ app(f, x) ∈ y /\ y ∈ B |- preimage(f, X, Y, y) ∈ preimages(f, X, Y, B)) by Tautology.from( + lastStep, + preimagesMembership of (A := B, x := preimage(f, X, Y, y)), + yInY, + preimageSubset of (A := y), + powerAxiom of (x := preimage(f, X, Y, y), y := X) + ) + have(x ∈ X /\ app(f, x) ∈ y /\ y ∈ B |- x ∈ preimage(f, X, Y, y) /\ preimage(f, X, Y, y) ∈ preimages(f, X, Y, B)) by Tautology.from( + lastStep, + preimageMembership of (B := y), + yInY + ) + thenHave(x ∈ X /\ app(f, x) ∈ y /\ y ∈ B |- ∃(z, x ∈ z /\ z ∈ preimages(f, X, Y, B))) by RightExists + have((x ∈ X, app(f, x) ∈ y /\ y ∈ B) |- x ∈ union(preimages(f, X, Y, B))) by Tautology.from( + lastStep, + unionAxiom of (z := x, x := preimages(f, X, Y, B)) + ) + thenHave((x ∈ X, ∃(y, app(f, x) ∈ y /\ y ∈ B)) |- x ∈ union(preimages(f, X, Y, B))) by LeftExists + have(thesis) by Tautology.from( + preimageMembership of (B := union(B)), + subsetClosedUnion of (x := B, y := Y), + unionAxiom of (z := app(f, x), x := B), + lastStep + ) + } + + val backward = have(x ∈ union(preimages(f, X, Y, B)) ==> x ∈ preimage(f, X, Y, union(B))) subproof { + assume(x ∈ union(preimages(f, X, Y, B))) + + val bSubsetY = have(b ∈ B |- b ⊆ Y) by Tautology.from( + subsetTactic of (x := B, y := powerSet(Y), z := b), + powerAxiom of (x := b, y := Y) + ) + have(x ∈ X /\ app(f, x) ∈ b /\ b ∈ B |- x ∈ X /\ app(f, x) ∈ b /\ b ∈ B) by Tautology + thenHave(x ∈ X /\ app(f, x) ∈ b /\ b ∈ B |- ∃(b, x ∈ X /\ app(f, x) ∈ b /\ b ∈ B)) by RightExists + have(x ∈ X /\ app(f, x) ∈ b /\ b ∈ B |- x ∈ preimage(f, X, Y, union(B))) by Tautology.from( + lastStep, + preimageMembership of (B := union(B)), + subsetClosedUnion of (x := B, y := Y), + unionAxiom of (z := app(f, x), x := B) + ) + have((x ∈ preimage(f, X, Y, b), b ∈ B) |- x ∈ preimage(f, X, Y, union(B))) by Tautology.from( + lastStep, + preimageMembership of (B := b), + bSubsetY + ) + have((x ∈ z, (z === preimage(f, X, Y, b)) /\ b ∈ B) |- x ∈ preimage(f, X, Y, union(B))) by Tautology.from( + lastStep, + replaceEqualityContainsRight of (x := z, y := preimage(f, X, Y, b), z := x) + ) + thenHave((x ∈ z, ∃(b, (z === preimage(f, X, Y, b)) /\ b ∈ B)) |- x ∈ preimage(f, X, Y, union(B))) by LeftExists + have(x ∈ z /\ z ∈ preimages(f, X, Y, B) |- x ∈ preimage(f, X, Y, union(B))) by Tautology.from( + lastStep, + preimagesMembership of (A := B, x := z) + ) + thenHave(∃(z, x ∈ z /\ z ∈ preimages(f, X, Y, B)) |- x ∈ preimage(f, X, Y, union(B))) by LeftExists + have(thesis) by Tautology.from( + lastStep, + unionAxiom of (z := x, x := preimages(f, X, Y, B)) + ) + } + + have(x ∈ preimage(f, X, Y, union(B)) <=> x ∈ union(preimages(f, X, Y, B))) by RightIff(forward, backward) + thenHave(∀(x, x ∈ preimage(f, X, Y, union(B)) <=> x ∈ union(preimages(f, X, Y, B)))) by RightForall + andThen(Substitution.applySubst(extensionalityAxiom of (x := preimage(f, X, Y, union(B)), y := union(preimages(f, X, Y, B))))) + } + + inline def directImagesFormula = y ∈ s <=> (y ∈ powerSet(Y) /\ ∃(a, a ∈ A /\ (y === directImage(f, X, Y, a)))) + + val directImagesUniqueness = Theorem( + (functionFrom(f, X, Y), A ⊆ powerSet(X)) |- ∃!(s, ∀(y, directImagesFormula)) + ) { + have(∃!(s, ∀(y, directImagesFormula))) by UniqueComprehension(powerSet(Y), lambda(y, ∃(a, a ∈ A /\ (y === directImage(f, X, Y, a))))) + thenHave(thesis) by Weakening + } + + /** + * Set of direct images of a set of subsets + * { f(A_i) | A_i ∈ A } + */ + val directImages = DEF(f, X, Y, A) --> TheConditional(s, ∀(y, directImagesFormula))(directImagesUniqueness) + + /** + * Useful statement about membership in the direct images + */ + val directImagesMembership = Theorem((functionFrom(f, X, Y), A ⊆ powerSet(X)) |- y ∈ directImages(f, X, Y, A) <=> (y ∈ powerSet(Y) /\ ∃(a, a ∈ A /\ (y === directImage(f, X, Y, a))))) { + assume(functionFrom(f, X, Y) /\ A ⊆ powerSet(X)) + have(∀(y, y ∈ directImages(f, X, Y, A) <=> (y ∈ powerSet(Y) /\ ∃(a, a ∈ A /\ (y === directImage(f, X, Y, a)))))) by InstantiateForall(directImages(f, X, Y, A))(directImages.definition) + thenHave(thesis) by InstantiateForall(y) + } + + /** + * Theorem -- generalization of `directImageSetUnion` + * The direct image of an arbitrary union is the union of the direct images + * f(⋃A) = ⋃(f(A)) + * + * This is why we needed the definition of `directImages`! + */ + val directImageUnionThm = Theorem( + (functionFrom(f, X, Y), A ⊆ powerSet(X)) |- + directImage(f, X, Y, union(A)) === union(directImages(f, X, Y, A)) + ) { + assume(functionFrom(f, X, Y), A ⊆ powerSet(X)) + + val forward = have(z ∈ directImage(f, X, Y, union(A)) ==> z ∈ union(directImages(f, X, Y, A))) subproof { + assume(z ∈ directImage(f, X, Y, union(A))) + + have(z ∈ Y /\ (app(f, x) === z) /\ x ∈ y /\ y ∈ A |- directImage(f, X, Y, y) ∈ directImages(f, X, Y, A) /\ z ∈ directImage(f, X, Y, y)) subproof { + assume(z ∈ Y, app(f, x) === z, x ∈ y, y ∈ A) + + val ySubsetX = have(y ⊆ X) by Tautology.from( + subsetTactic of (x := A, y := powerSet(X), z := y), + powerAxiom of (x := y, y := X) + ) + + val p1 = have(directImage(f, X, Y, y) ∈ powerSet(Y)) by Tautology.from( + powerAxiom of (x := directImage(f, X, Y, y), y := Y), + directImageSubsetCodomain of (A := y), + functionImpliesRangeSubsetOfCodomain of (x := X, y := Y), + subsetTransitivity of (a := directImage(f, X, Y, y), b := functionRange(f), c := Y), + subsetTactic of (x := A, y := powerSet(X), z := y), + powerAxiom of (x := y, y := X) + ) + + have(y ∈ A /\ (directImage(f, X, Y, y) === directImage(f, X, Y, y))) by Tautology.from( + equalityReflexivity of (x := y) + ) + val p2 = thenHave(∃(a, a ∈ A /\ (directImage(f, X, Y, y) === directImage(f, X, Y, a)))) by RightExists + + val p3 = have(directImage(f, X, Y, y) ∈ directImages(f, X, Y, A)) by Tautology.from(p1, p2, directImagesMembership of (y := directImage(f, X, Y, y))) + + have((app(f, x) === z) /\ x ∈ y) by Tautology + thenHave(exists(x, (app(f, x) === z) /\ x ∈ y)) by RightExists + val p4 = have(z ∈ directImage(f, X, Y, y)) by Tautology.from(lastStep, directImageMembership of (y := z, A := y), ySubsetX) + + have(thesis) by Tautology.from(p3, p4) + } + thenHave(z ∈ Y /\ (app(f, x) === z) /\ x ∈ y /\ y ∈ A |- directImage(f, X, Y, y) ∈ directImages(f, X, Y, A) /\ z ∈ directImage(f, X, Y, y)) by Tautology + thenHave(z ∈ Y /\ (app(f, x) === z) /\ x ∈ y /\ y ∈ A |- ∃(y, y ∈ directImages(f, X, Y, A) /\ z ∈ y)) by RightExists + have((z ∈ Y, (app(f, x) === z), x ∈ y /\ y ∈ A) |- z ∈ union(directImages(f, X, Y, A))) by Tautology.from( + lastStep, + unionAxiom of (x := directImages(f, X, Y, A)) + ) + thenHave((z ∈ Y, (app(f, x) === z), ∃(y, y ∈ A /\ x ∈ y)) |- z ∈ union(directImages(f, X, Y, A))) by LeftExists + have(z ∈ Y /\ (app(f, x) === z) /\ x ∈ union(A) |- z ∈ union(directImages(f, X, Y, A))) by Tautology.from( + lastStep, + unionAxiom of (z := x, x := A) + ) + thenHave(∃(x, z ∈ Y /\ (app(f, x) === z) /\ x ∈ union(A)) |- z ∈ union(directImages(f, X, Y, A))) by LeftExists + have(thesis) by Tautology.from( + lastStep, + subsetClosedUnion of (x := A, y := X), + directImageMembership of (y := z, A := union(A)) + ) + } + + val backward = have(z ∈ union(directImages(f, X, Y, A)) ==> z ∈ directImage(f, X, Y, union(A))) subproof { + have(z ∈ Y /\ (app(f, x) === z) /\ x ∈ a /\ a ∈ A |- z ∈ Y /\ (app(f, x) === z) /\ x ∈ a /\ a ∈ A) by Tautology + thenHave(z ∈ Y /\ (app(f, x) === z) /\ x ∈ a /\ a ∈ A |- ∃(a, z ∈ Y /\ (app(f, x) === z) /\ x ∈ a /\ a ∈ A)) by RightExists + have(z ∈ Y /\ (app(f, x) === z) /\ x ∈ a /\ a ∈ A |- z ∈ Y /\ (app(f, x) === z) /\ x ∈ union(A)) by Tautology.from( + lastStep, + unionAxiom of (z := x, x := A) + ) + thenHave(z ∈ Y /\ (app(f, x) === z) /\ x ∈ a /\ a ∈ A |- ∃(x, z ∈ Y /\ (app(f, x) === z) /\ x ∈ union(A))) by RightExists + have((z ∈ Y, (app(f, x) === z) /\ x ∈ a, a ∈ A) |- z ∈ directImage(f, X, Y, union(A))) by Tautology.from( + lastStep, + directImageMembership of (y := z, A := union(A)), + subsetClosedUnion of (x := A, y := X) + ) + thenHave((z ∈ Y, ∃(x, (app(f, x) === z) /\ x ∈ a), a ∈ A) |- z ∈ directImage(f, X, Y, union(A))) by LeftExists + have(z ∈ directImage(f, X, Y, a) /\ a ∈ A |- z ∈ directImage(f, X, Y, union(A))) by Tautology.from( + lastStep, + directImageMembership of (y := z, A := a), + subsetClosedUnion of (x := A, y := X), + subsetTactic of (x := A, y := powerSet(X), z := a), + powerAxiom of (x := a, y := X) + ) + have((z ∈ y, a ∈ A /\ (y === directImage(f, X, Y, a)), y ∈ powerSet(Y)) |- z ∈ directImage(f, X, Y, union(A))) by Tautology.from( + lastStep, + replaceEqualityContainsRight of (x := y, y := directImage(f, X, Y, a)), + directImageSubsetCodomain of (A := a), + functionImpliesRangeSubsetOfCodomain of (x := X, y := Y), + subsetTransitivity of (a := directImage(f, X, Y, a), b := functionRange(f), c := Y), + powerAxiom of (x := directImage(f, X, Y, a), y := Y), + replaceEqualityContainsLeft of (x := y, y := directImage(f, X, Y, a), z := powerSet(Y)) + ) + thenHave( + (z ∈ y, ∃(a, a ∈ A /\ (y === directImage(f, X, Y, a))), y ∈ powerSet(Y)) + |- z ∈ directImage(f, X, Y, union(A)) + ) by LeftExists + have(z ∈ y /\ y ∈ directImages(f, X, Y, A) |- z ∈ directImage(f, X, Y, union(A))) by Tautology.from( + lastStep, + directImagesMembership + ) + thenHave(∃(y, z ∈ y /\ y ∈ directImages(f, X, Y, A)) |- z ∈ directImage(f, X, Y, union(A))) by LeftExists + have(z ∈ union(directImages(f, X, Y, A)) |- z ∈ directImage(f, X, Y, union(A))) by Tautology.from( + lastStep, + unionAxiom of (x := directImages(f, X, Y, A)) + ) + } + + have(z ∈ directImage(f, X, Y, union(A)) <=> z ∈ union(directImages(f, X, Y, A))) by RightIff(forward, backward) + thenHave(∀(z, z ∈ directImage(f, X, Y, union(A)) <=> z ∈ union(directImages(f, X, Y, A)))) by RightForall + andThen(Substitution.applySubst(extensionalityAxiom of (x := directImage(f, X, Y, union(A)), y := union(directImages(f, X, Y, A))))) + } + + /** + * Theorem -- the direct image of the preimage is always a subset of the original set + * f(f^(-1)(A)) ⊆ A + */ + val directImagePreimage = Theorem( + (functionFrom(f, X, Y), subset(A, Y)) + |- directImage(f, X, Y, preimage(f, X, Y, A)) ⊆ A + ) { + assume(functionFrom(f, X, Y), subset(A, Y)) + have(subset(preimage(f, X, Y, A), X) |- ∀(z, z ∈ directImage(f, X, Y, preimage(f, X, Y, A)) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ preimage(f, X, Y, A))))) by InstantiateForall( + directImage(f, X, Y, preimage(f, X, Y, A)) + )(directImage.definition of (A := preimage(f, X, Y, A))) + thenHave(subset(preimage(f, X, Y, A), X) |- z ∈ directImage(f, X, Y, preimage(f, X, Y, A)) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ preimage(f, X, Y, A)))) by InstantiateForall(z) + val imageMember = have(z ∈ directImage(f, X, Y, preimage(f, X, Y, A)) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ preimage(f, X, Y, A)))) by Tautology.from(lastStep, preimageSubset) + + have(in(z, directImage(f, X, Y, preimage(f, X, Y, A))) ==> in(z, A)) subproof { + assume(in(z, directImage(f, X, Y, preimage(f, X, Y, A)))) + have(((app(f, x) === z), x ∈ preimage(f, X, Y, A)) |- (app(f, x) === z) /\ (x ∈ X /\ app(f, x) ∈ A)) by Tautology.from(preimageMembership of (B := A)) + have(((app(f, x) === z) /\ x ∈ preimage(f, X, Y, A)) |- in(z, A)) by Tautology.from(lastStep, replaceEqualityContainsLeft of (x := app(f, x), y := z, z := A)) + thenHave(exists(x, (app(f, x) === z) /\ x ∈ preimage(f, X, Y, A)) |- in(z, A)) by LeftExists + have(thesis) by Tautology.from(lastStep, imageMember) + } + thenHave(∀(z, in(z, directImage(f, X, Y, preimage(f, X, Y, A))) ==> in(z, A))) by RightForall + have(thesis) by Tautology.from(lastStep, subsetAxiom of (x := directImage(f, X, Y, preimage(f, X, Y, A)), y := A)) + } + + /** + * Theorem -- refinement of `directImagePreimage` in case of surjective functions (we have equality!) + */ + val directImagePreimageSurjective = Theorem( + (functionFrom(f, X, Y), surjective(f, X, Y), subset(A, Y)) + |- directImage(f, X, Y, preimage(f, X, Y, A)) === A + ) { + assume(functionFrom(f, X, Y), surjective(f, X, Y), subset(A, Y)) + + val forward = have(x ∈ directImage(f, X, Y, preimage(f, X, Y, A)) ==> x ∈ A) by Tautology.from( + subsetTactic of (x := directImage(f, X, Y, preimage(f, X, Y, A)), y := A, z := x), + directImagePreimage + ) + + val backward = have(y ∈ A ==> y ∈ directImage(f, X, Y, preimage(f, X, Y, A))) subproof { + assume(y ∈ A) + have(x ∈ functionDomain(f) /\ (app(f, x) === y) |- (app(f, x) === y) /\ x ∈ preimage(f, X, Y, A)) by Tautology.from( + functionFromImpliesDomainEq of (x := X, y := Y), + replaceEqualityContainsRight of (x := functionDomain(f), y := X, z := x), + replaceEqualityContainsLeft of (x := app(f, x), z := A), + preimageMembership of (B := A) + ) + thenHave(x ∈ functionDomain(f) /\ (app(f, x) === y) |- ∃(x, (app(f, x) === y) /\ x ∈ preimage(f, X, Y, A))) by RightExists + have(x ∈ functionDomain(f) /\ (app(f, x) === y) |- y ∈ directImage(f, X, Y, preimage(f, X, Y, A))) by Tautology.from( + lastStep, + subsetTactic of (x := A, y := Y, z := y), + directImageMembership of (A := preimage(f, X, Y, A)), + preimageSubset + ) + thenHave(∃(x, x ∈ functionDomain(f) /\ (app(f, x) === y)) |- y ∈ directImage(f, X, Y, preimage(f, X, Y, A))) by LeftExists + have(thesis) by Tautology.from( + lastStep, + functionRangeMembership, + subsetTactic of (x := A, y := Y, z := y), + surjectiveImpliesRangeIsCodomain of (x := X, y := Y), + replaceEqualityContainsRight of (x := Y, y := functionRange(f), z := y), + functionFromImpliesFunctional of (x := X, y := Y) + ) + } + + have(x ∈ directImage(f, X, Y, preimage(f, X, Y, A)) <=> x ∈ A) by RightIff(forward, backward of (y := x)) + thenHave(∀(x, x ∈ directImage(f, X, Y, preimage(f, X, Y, A)) <=> x ∈ A)) by RightForall + andThen(Substitution.applySubst(extensionalityAxiom of (x := directImage(f, X, Y, preimage(f, X, Y, A)), y := A))) + } + + /** + * Theorem -- the direct image of the domain is the function range + * f(X) = functionRange(f) + */ + val directImageX = Theorem( + functionFrom(f, X, Y) + |- directImage(f, X, Y, X) === functionRange(f) + ) { + assume(functionFrom(f, X, Y)) + + have(subset(X, X) |- ∀(z, z ∈ directImage(f, X, Y, X) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ X)))) by InstantiateForall(directImage(f, X, Y, X))(directImage.definition of (A := X)) + thenHave(subset(X, X) |- z ∈ directImage(f, X, Y, X) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ X))) by InstantiateForall(z) + val defIm = have(z ∈ directImage(f, X, Y, X) <=> (z ∈ Y /\ ∃(x, (app(f, x) === z) /\ x ∈ X))) by Tautology.from( + lastStep, + subsetReflexivity of (x := X) + ) + + val forward = have(z ∈ directImage(f, X, Y, X) ==> z ∈ functionRange(f)) by Tautology.from( + directImageSubsetCodomain of (A := X), + subsetReflexivity of (x := X), + subsetTactic of (x := directImage(f, X, Y, X), y := functionRange(f)) + ) + + val backward = have(z ∈ functionRange(f) ==> z ∈ directImage(f, X, Y, X)) subproof { + assume(z ∈ functionRange(f)) + + have(subset(functionRange(f), Y)) by Tautology.from(functionImpliesRangeSubsetOfCodomain of (x := X, y := Y)) + val zInY = have(z ∈ Y) by Tautology.from(lastStep, subsetTactic of (x := functionRange(f), y := Y)) + + have(x ∈ functionDomain(f) /\ (app(f, x) === z) |- x ∈ X /\ (app(f, x) === z)) by Tautology.from( + functionFromImpliesDomainEq of (x := X, y := Y), + replaceEqualityContainsRight of (x := functionDomain(f), y := X, z := x) + ) + thenHave(x ∈ functionDomain(f) /\ (app(f, x) === z) |- ∃(x, (app(f, x) === z) /\ x ∈ X)) by RightExists + have(x ∈ functionDomain(f) /\ (app(f, x) === z) |- z ∈ directImage(f, X, Y, X)) by Tautology.from( + lastStep, + defIm, + zInY + ) + thenHave(∃(x, x ∈ functionDomain(f) /\ (app(f, x) === z)) |- z ∈ directImage(f, X, Y, X)) by LeftExists + + have(thesis) by Tautology.from( + lastStep, + functionRangeMembership of (y := z), + functionFromImpliesFunctional of (x := X, y := Y) + ) + } + + have(z ∈ directImage(f, X, Y, X) <=> z ∈ functionRange(f)) by RightIff(forward, backward) + thenHave(∀(z, z ∈ directImage(f, X, Y, X) <=> z ∈ functionRange(f))) by RightForall + andThen(Substitution.applySubst(extensionalityAxiom of (x := directImage(f, X, Y, X), y := functionRange(f)))) + } + + /** + * Theorem -- the direct image of the domain is precisely Y if the function is surjective + * f(X) = Y + */ + val imageSurjective = Theorem( + (functionFrom(f, X, Y), surjective(f, X, Y)) |- directImage(f, X, Y, X) === Y + ) { + have(thesis) by Tautology.from( + surjectiveImpliesRangeIsCodomain of (x := X, y := Y), + directImageX, + equalityTransitivity of (x := Y, y := functionRange(f), z := directImage(f, X, Y, X)) + ) + } +} diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/functions/package.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/functions/package.scala index ec68adf10..074c0d757 100644 --- a/lisa-sets/src/main/scala/lisa/maths/settheory/functions/package.scala +++ b/lisa-sets/src/main/scala/lisa/maths/settheory/functions/package.scala @@ -71,4 +71,27 @@ package object functions { constantFunctionFunctionFrom, constantFunctionApplication } + /*export lisa.maths.settheory.functions.DirectPreimages.{ + directImage, + directImageMembership, + directImageSetUnion, + preimage, + preimageMembership, + preimageSubset, + preimageY, + preimages, + preimagesMembership, + directImages, + directImagesMembership, + preimageSetUnion, + preimageDifference, + preimageUnionThm, + directImageEmptySet, + directImageSubset, + applyDirectImage, + directImagePreimage, + directImagePreimageSurjective, + directImageX, + imageSurjective + }*/ } diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala index 7a05b0b49..9a0c92fbf 100644 --- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala +++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala @@ -5,6 +5,7 @@ package lisa.maths.settheory.types.adt import lisa.maths.settheory.SetTheory.{*, given} + import ADTDefinitions.* import Helpers.* diff --git a/lisa-topology/src/main/scala/lisa/maths/topology/Compactness.scala b/lisa-topology/src/main/scala/lisa/maths/topology/Compactness.scala new file mode 100644 index 000000000..a6fcc1233 --- /dev/null +++ b/lisa-topology/src/main/scala/lisa/maths/topology/Compactness.scala @@ -0,0 +1,390 @@ +package lisa.maths.topology + +import lisa.automation.settheory.SetTheoryTactics.* +import lisa.maths.Quantifiers.* + +import lisa.automation.kernel.CommonTactics.Definition + +import lisa.maths.topology.Topology.* +import lisa.maths.topology.Continuity.* +import lisa.maths.settheory.* +import lisa.maths.settheory.SetTheory.* +import lisa.maths.settheory.SetTheoryBasics.* +import lisa.automation.kernel.CommonTactics.* +import lisa.automation.settheory.SetTheoryTactics.UniqueComprehension +import lisa.automation.settheory.SetTheoryTactics.TheConditional +import lisa.maths.settheory.functions.Functionals.* +import lisa.maths.settheory.functions.DirectPreimages.* + +object Compactness extends lisa.Main { + // var defs + private val x, y, z, a, b, c, t, p, f, r, s = variable + private val X, T, T1, T2 = variable + private val S, A, B, Y, o, O, O2, O3 = variable + + // ------------------- + // Compactness + // ------------------- + + // A cover of X is a set of subsets of X that covers X (i.e. their union is a superset of X) + val cover = DEF(X, O) --> + ∀(o, in(o, O) ==> subset(o, X)) /\ + subset(X, union(O)) + + // Open cover is a cover that is a set of open sets! + val openCover = DEF(X, T, O) --> + cover(X, O) /\ subset(O, T) + + // TODO: we need a notion of finiteness/cardinality for that + val finite = DEF(X) --> (X === emptySet) + + /* + * Compact spaces + * A topological space is compact if every open cover has a finite subcover + */ + val compact = DEF(X, T) --> + topology(X, T) /\ + ∀( + O, + openCover(X, T, O) ==> + ∃( + O2, // Another subcovering + subset(O2, O) /\ cover(X, O2) /\ finite(O2) + ) + ) + + /** + * Intermediate lemma for theorem below + * about covering the directImage with directImages + */ + val coverDirectImage = Theorem( + (functionFrom(f, X, Y), A ⊆ powerSet(X), cover(X, A)) |- cover(directImage(f, X, Y, X), directImages(f, X, Y, A)) + ) { + assume(functionFrom(f, X, Y), A ⊆ powerSet(X), cover(X, A)) + + // Part 1 + have(X ⊆ union(A)) by Tautology.from(cover.definition of (X := X, O := A)) + have(directImage(f, X, Y, X) ⊆ directImage(f, X, Y, union(A))) by Tautology.from( + directImageMonotonicity of (A := X, B := union(A)), + subsetClosedUnion of (x := A, y := X), + lastStep + ) + val isSubset = have(directImage(f, X, Y, X) ⊆ union(directImages(f, X, Y, A))) by Tautology.from( + lastStep, + directImageUnionThm, + replaceEqualitySubsetRight of (z := directImage(f, X, Y, X), x := union(directImages(f, X, Y, A)), y := directImage(f, X, Y, union(A))) + ) + + // Part 2 + have(a ∈ A /\ (o === directImage(f, X, Y, a)) |- o ⊆ directImage(f, X, Y, X)) by Tautology.from( + subsetTactic of (x := A, y := powerSet(X), z := a), + powerAxiom of (x := a, y := X), + directImageMonotonicity of (A := a, B := X), + subsetReflexivity of (x := X), + equalityBySubset of (x := o, y := directImage(f, X, Y, a)), + subsetTransitivity of (a := o, b := directImage(f, X, Y, a), c := directImage(f, X, Y, X)) + ) + thenHave(∃(a, a ∈ A /\ (o === directImage(f, X, Y, a))) |- o ⊆ directImage(f, X, Y, X)) by LeftExists + have(o ∈ directImages(f, X, Y, A) |- o ⊆ directImage(f, X, Y, X)) by Tautology.from( + lastStep, + directImagesMembership of (y := o) + ) + thenHave(o ∈ directImages(f, X, Y, A) ==> o ⊆ directImage(f, X, Y, X)) by Tautology + val elementsSubsets = thenHave(∀(o, o ∈ directImages(f, X, Y, A) ==> o ⊆ directImage(f, X, Y, X))) by RightForall + + // Conclude + have(thesis) by Tautology.from(isSubset, elementsSubsets, cover.definition of (X := directImage(f, X, Y, X), O := directImages(f, X, Y, A))) + } + + /** + * Lemma -- + * Any subset of an open cover is an open cover + */ + val subsetOpenCover = Theorem( + (openCover(X, T, O), subset(O2, O), cover(X, O2)) |- openCover(X, T, O2) + ) { + assume(openCover(X, T, O), O2 ⊆ O, cover(X, O2)) + + have(thesis) by Tautology.from( + openCover.definition of (O := O2), + openCover.definition, + subsetTransitivity of (a := O2, b := O, c := T) + ) + } + + /** + * Lemma -- + * The preimages of some set in P(Y) are in P(X) + */ + val preimagesInPowerSet = Theorem( + (functionFrom(f, X, Y), A ⊆ powerSet(Y)) |- preimages(f, X, Y, A) ⊆ powerSet(X) + ) { + assume(functionFrom(f, X, Y), A ⊆ powerSet(Y)) + + have(x ∈ preimages(f, X, Y, A) ==> x ∈ powerSet(X)) by Tautology.from( + preimagesMembership of (A := A, x := x) + ) + thenHave(∀(x, x ∈ preimages(f, X, Y, A) ==> x ∈ powerSet(X))) by RightForall + have(thesis) by Tautology.from(lastStep, subsetAxiom of (x := preimages(f, X, Y, A), y := powerSet(X))) + } + + /** + * Lemma -- + * The set of direct images is finite + */ + val directImageFinite = Theorem( + (functionFrom(f, X, Y), A ⊆ powerSet(X), finite(A)) |- finite(directImages(f, X, Y, A)) + ) { + assume(functionFrom(f, X, Y), A ⊆ powerSet(X), finite(A)) + // TODO: Needs to have a notion of finiteness to complete the proof + // Normally it should just be because there is a bijection between directImages(f, X, Y, A) and A, and A is finite + sorry + } + + /** + * The image of a compact space by a continuous, surjective mapping is a compact space + */ + val imageCompactThm = Theorem((compact(X, T1), continuous(f, X, T1, Y, T2), surjective(f, X, Y)) |- compact(Y, T2)) { + assume(compact(X, T1), continuous(f, X, T1, Y, T2), surjective(f, X, Y)) + + val xIsTop = have(topology(X, T1)) by Tautology.from(continuous.definition, mapping.definition) + val yIsTop = have(topology(Y, T2)) by Tautology.from(continuous.definition, mapping.definition) + + val xIsCompact = have(∀(O, openCover(X, T1, O) ==> ∃(O2, subset(O2, O) /\ cover(X, O2) /\ finite(O2)))) by Tautology.from( + compact.definition of (T := T1) + ) + val isContinuous = have(∀(O, O ∈ T2 ==> preimage(f, X, Y, O) ∈ T1)) by Tautology.from(continuous.definition) + + val fIsFunction = have(functionFrom(f, X, Y)) by Tautology.from(continuous.definition, mapping.definition) + + have(openCover(Y, T2, O) |- ∃(O2, subset(O2, O) /\ cover(Y, O2) /\ finite(O2))) subproof { + assume(openCover(Y, T2, O)) + + have(∀(O, (O ⊆ T2) ==> (union(O) ∈ T2))) by Tautology.from( + containsUnion.definition of (T := T2), + yIsTop, + topology.definition of (X := Y, T := T2) + ) + thenHave(O ⊆ T2 ==> (union(O) ∈ T2)) by InstantiateForall(O) + val unionInT2 = have(union(O) ∈ T2) by Tautology.from( + openCover.definition of (X := Y, T := T2), + lastStep + ) + + val oInPowerSet = have(O ⊆ powerSet(Y)) by Tautology.from( + openCover.definition of (X := Y, T := T2), + yIsTop, + topology.definition of (X := Y, T := T2), + setOfSubsets.definition of (X := Y, T := T2), + subsetTransitivity of (a := O, b := T2, c := powerSet(Y)) + ) + val unionOSubsetY = have(union(O) ⊆ Y) by Tautology.from( + oInPowerSet, + subsetClosedUnion of (x := O, y := Y) + ) + + // We have an open cover of X, that's preimages(f, X, Y, O) + val isOpenCover = have(openCover(X, T1, preimages(f, X, Y, O))) subproof { + // Firstly, it's a cover + val isCover = have(cover(X, preimages(f, X, Y, O))) subproof { + have(o ∈ preimages(f, X, Y, O) ==> o ⊆ X) subproof { + assume(o ∈ preimages(f, X, Y, O)) + have(o ∈ powerSet(X)) by Tautology.from( + preimagesMembership of (A := O, x := o), + fIsFunction, + oInPowerSet + ) + have(o ⊆ X) by Tautology.from(lastStep, powerAxiom of (x := o, y := X)) + } + val firstPart = thenHave(∀(o, o ∈ preimages(f, X, Y, O) ==> o ⊆ X)) by RightForall + + // The covering part + have(x ∈ X ==> x ∈ union(preimages(f, X, Y, O))) subproof { + assume(x ∈ X) + // Function application + have(app(f, x) ∈ Y) by Tautology.from( + fIsFunction, + lastStep, + functionFromApplication of (x := X, y := Y, a := x), + functionFrom.definition of (x := X, y := Y) + ) + // Since Y is covered by O + have(app(f, x) ∈ union(O)) by Tautology.from( + lastStep, + openCover.definition of (X := Y, T := T2), + cover.definition of (X := Y), + subsetTactic of (x := Y, y := union(O), z := app(f, x)) + ) + // That's the definition of being in the preimage! + have(x ∈ preimage(f, X, Y, union(O))) by Tautology.from( + lastStep, + preimageMembership of (B := union(O)), + fIsFunction, + unionOSubsetY + ) + // use that preimage(f, X, Y, union(O)) ⊆ union(preimages(f, X, Y, O)) + have(x ∈ union(preimages(f, X, Y, O))) by Tautology.from( + lastStep, + preimageUnionThm of (B := O), + replaceEqualityContainsRight of (x := preimage(f, X, Y, union(O)), y := union(preimages(f, X, Y, O)), z := x), + fIsFunction, + oInPowerSet + ) + } + thenHave(∀(x, x ∈ X ==> x ∈ union(preimages(f, X, Y, O)))) by RightForall + val secondPart = have(subset(X, union(preimages(f, X, Y, O)))) by Tautology.from( + lastStep, + subsetAxiom of (x := X, y := union(preimages(f, X, Y, O))) + ) + + have(thesis) by Tautology.from(firstPart, secondPart, cover.definition of (O := preimages(f, X, Y, O))) + } + + // Also, its elements are open + have(z ∈ preimages(f, X, Y, O) ==> z ∈ T1) subproof { + assume(z ∈ preimages(f, X, Y, O)) + val existsa = have(∃(a, a ∈ O /\ (z === preimage(f, X, Y, a)))) by Tautology.from( + lastStep, + preimagesMembership of (A := O, x := z), + fIsFunction, + oInPowerSet + ) + have(a ∈ O /\ (z === preimage(f, X, Y, a)) |- z ∈ T1) subproof { + assume(a ∈ O /\ (z === preimage(f, X, Y, a))) + val aInT2 = have(a ∈ T2) by Tautology.from( + openCover.definition of (X := Y, T := T2), + subsetTactic of (x := O, y := T2, z := a) + ) + have(a ∈ T2 ==> preimage(f, X, Y, a) ∈ T1) by InstantiateForall(a)(isContinuous) + have(preimage(f, X, Y, a) ∈ T1) by Tautology.from( + aInT2, + lastStep + ) + have(z ∈ T1) by Tautology.from(lastStep, replaceEqualityContainsLeft of (x := z, y := preimage(f, X, Y, a), z := T1)) + } + thenHave(∃(a, a ∈ O /\ (z === preimage(f, X, Y, a))) |- z ∈ T1) by LeftExists + have(thesis) by Tautology.from(existsa, lastStep) + } + thenHave(∀(z, z ∈ preimages(f, X, Y, O) ==> z ∈ T1)) by RightForall + val isOpenSubset = have(preimages(f, X, Y, O) ⊆ T1) by Tautology.from( + subsetAxiom of (x := preimages(f, X, Y, O), y := T1), + lastStep + ) + + have(thesis) by Tautology.from(openCover.definition of (T := T1, O := preimages(f, X, Y, O)), isCover, isOpenSubset) + } + + // Whence the existence of a finite subcover O3 + have(openCover(X, T1, preimages(f, X, Y, O)) ==> ∃(O3, subset(O3, preimages(f, X, Y, O)) /\ cover(X, O3) /\ finite(O3))) by InstantiateForall(preimages(f, X, Y, O))( + xIsCompact + ) + val existsO3 = have(∃(O3, subset(O3, preimages(f, X, Y, O)) /\ cover(X, O3) /\ finite(O3))) by Tautology.from(lastStep, isOpenCover) + + have( + O3 ⊆ preimages(f, X, Y, O) /\ cover(X, O3) /\ finite(O3) + |- + subset(directImages(f, X, Y, O3), O) /\ cover(Y, directImages(f, X, Y, O3)) /\ finite(directImages(f, X, Y, O3)) + ) subproof { + assume(O3 ⊆ preimages(f, X, Y, O), cover(X, O3), finite(O3)) + + val o3InPowerSet = have(O3 ⊆ powerSet(X)) subproof { + have(preimages(f, X, Y, O) ⊆ powerSet(X)) by Tautology.from( + fIsFunction, + oInPowerSet, + preimagesInPowerSet of (A := O) + ) + have(thesis) by Tautology.from(lastStep, subsetTransitivity of (a := O3, b := preimages(f, X, Y, O), c := powerSet(X))) + } + + // So it's a subset + have(z ∈ directImages(f, X, Y, O3) ==> z ∈ O) subproof { + assume(z ∈ directImages(f, X, Y, O3)) + + have(z ∈ powerSet(Y) /\ ∃(a, a ∈ O3 /\ (z === directImage(f, X, Y, a)))) by Tautology.from( + directImagesMembership of (A := O3, y := z), + fIsFunction, + o3InPowerSet + ) + + have(a ∈ O3 /\ (z === directImage(f, X, Y, a)) |- z ∈ O) subproof { + assume(a ∈ O3, z === directImage(f, X, Y, a)) + val aInPreimages = have(a ∈ preimages(f, X, Y, O)) by Tautology.from( + lastStep, + subsetTactic of (x := O3, y := preimages(f, X, Y, O), z := a) + ) + have(b ∈ O /\ (a === preimage(f, X, Y, b)) |- directImage(f, X, Y, a) ∈ O) subproof { + assume(b ∈ O, a === preimage(f, X, Y, b)) + have(b ⊆ Y) by Tautology.from( + oInPowerSet, + subsetTactic of (z := b, x := O, y := powerSet(Y)), + powerAxiom of (x := b, y := Y) + ) + val statement = have(directImage(f, X, Y, preimage(f, X, Y, b)) === b) by Tautology.from( + lastStep, + directImagePreimageSurjective of (A := b), + fIsFunction + ) + thenHave(directImage(f, X, Y, a) === b) by RightSubstEq.withParametersSimple(List((a, preimage(f, X, Y, b))), lambda(x, directImage(f, X, Y, x) === b)) + have(thesis) by Tautology.from(lastStep, replaceEqualityContainsLeft of (x := directImage(f, X, Y, a), y := b, z := O)) + } + thenHave(exists(b, b ∈ O /\ (a === preimage(f, X, Y, b))) |- directImage(f, X, Y, a) ∈ O) by LeftExists + // use that (functionFrom(f, X, Y), O ⊆ powerSet(Y)) |- a ∈ preimages(f, X, Y, O) ==> (∃(b, b ∈ O /\ (a === preimage(f, X, Y, b))))) + have(directImage(f, X, Y, a) ∈ O) by Tautology.from(lastStep, aInPreimages, preimagesMembership of (A := O, x := a), fIsFunction, oInPowerSet) + // Conclude since z === directImage(f, X, Y, a) + have(z ∈ O) by Tautology.from(lastStep, replaceEqualityContainsLeft of (x := z, y := directImage(f, X, Y, a), z := O)) + } + + thenHave(∃(a, a ∈ O3 /\ (z === directImage(f, X, Y, a))) |- z ∈ O) by LeftExists + + // Since z is in directImages, then we precisely have ∃(a, a ∈ O3 /\ (z === directImage(f, X, Y, a))) by `directImagesMembership` + have(thesis) by Tautology.from(lastStep, directImagesMembership of (A := O3, y := z), fIsFunction, o3InPowerSet) + } + thenHave(∀(z, z ∈ directImages(f, X, Y, O3) ==> z ∈ O)) by RightForall + val isSubset = have(directImages(f, X, Y, O3) ⊆ O) by Tautology.from(lastStep, subsetAxiom of (x := directImages(f, X, Y, O3), y := O)) + + // That is also covering Y + // We use that f is surjective to get that directImage(f, X, Y, X) = Y + val replacement = have(directImage(f, X, Y, X) === Y) by Tautology.from(imageSurjective, fIsFunction) + val coveringStatement = have(cover(directImage(f, X, Y, X), directImages(f, X, Y, O3))) by Tautology.from( + coverDirectImage of (A := O3), + fIsFunction, + o3InPowerSet + ) + have( + ((directImage(f, X, Y, X) === Y), cover(directImage(f, X, Y, X), directImages(f, X, Y, O3))) + |- cover(Y, directImages(f, X, Y, O3)) + ) subproof { + have( + ((directImage(f, X, Y, X) === Y), cover(directImage(f, X, Y, X), directImages(f, X, Y, O3))) + |- cover(directImage(f, X, Y, X), directImages(f, X, Y, O3)) + ) by Tautology + thenHave(thesis) by RightSubstEq.withParametersSimple(List((directImage(f, X, Y, X), Y)), lambda(x, cover(x, directImages(f, X, Y, O3)))) + } + val covering = have(cover(Y, directImages(f, X, Y, O3))) by Tautology.from(lastStep, coveringStatement, replacement) + + // Finally it's finite since O3 is + val finiteCover = have(finite(directImages(f, X, Y, O3))) by Tautology.from( + directImageFinite of (A := O3), + fIsFunction, + o3InPowerSet + ) + + have(thesis) by Tautology.from(isSubset, finiteCover, covering) + } + + thenHave( + subset(O3, preimages(f, X, Y, O)) /\ cover(X, O3) /\ finite(O3) + |- + ∃(O2, subset(O2, O) /\ cover(Y, O2) /\ finite(O2)) + ) by RightExists + + // Concluding + thenHave(∃(O3, subset(O3, preimages(f, X, Y, O)) /\ cover(X, O3) /\ finite(O3)) |- ∃(O2, subset(O2, O) /\ cover(Y, O2) /\ finite(O2))) by LeftExists + have(thesis) by Tautology.from(lastStep, existsO3) + } + thenHave(openCover(Y, T2, O) ==> ∃(O2, subset(O2, O) /\ cover(Y, O2) /\ finite(O2))) by Tautology + val yIsCompact = thenHave(∀(O, openCover(Y, T2, O) ==> ∃(O2, subset(O2, O) /\ cover(Y, O2) /\ finite(O2)))) by RightForall + + have(thesis) by Tautology.from(yIsCompact, yIsTop, compact.definition of (X := Y, T := T2)) + } +} diff --git a/lisa-topology/src/main/scala/lisa/maths/topology/Continuity.scala b/lisa-topology/src/main/scala/lisa/maths/topology/Continuity.scala new file mode 100644 index 000000000..b7c7e6993 --- /dev/null +++ b/lisa-topology/src/main/scala/lisa/maths/topology/Continuity.scala @@ -0,0 +1,159 @@ +package lisa.maths.topology + +import lisa.automation.settheory.SetTheoryTactics.* +import lisa.maths.Quantifiers.* + +import lisa.automation.kernel.CommonTactics.Definition + +import lisa.maths.topology.Topology.* +import lisa.maths.settheory.* +import lisa.maths.settheory.SetTheory.* +import lisa.maths.settheory.SetTheoryBasics.* +import lisa.automation.kernel.CommonTactics.* +import lisa.automation.settheory.SetTheoryTactics.UniqueComprehension +import lisa.automation.settheory.SetTheoryTactics.TheConditional +import lisa.maths.settheory.functions.Functionals.* +import lisa.maths.settheory.functions.DirectPreimages.* + +object Continuity extends lisa.Main { + // var defs + private val x, y, z, a, b, c, t, p, f, r, s = variable + private val X, T, T1, T2 = variable + private val S, A, B, Y, o, O, O2, O3 = variable + + // ------------------- + // Mappings + // ------------------- + /* + * A mapping is a function between topological spaces + */ + val mapping = DEF(f, X, T1, Y, T2) --> + (functionFrom(f, X, Y) /\ topology(X, T1) /\ topology(Y, T2)) + + // ------------------- + // Continuity + // ------------------- + /** + * A function f is continuous if the preimage of any open set in the codomain is open in the domain + */ + val continuous = DEF(f, X, T1, Y, T2) --> + (mapping(f, X, T1, Y, T2) /\ ∀(O, O ∈ T2 ==> preimage(f, X, Y, O) ∈ T1)) + + // ------------------- + // Connectedness + // ------------------- + /* + * A set A is clopen if it is both open and closed + */ + val clopen = DEF(X, T, A) --> ( + topology(X, T) /\ + A ∈ T /\ setDifference(X, A) ∈ T + ) + + /** + * A topological space is connected if the only clopen sets are the empty set and the whole space + */ + val connectedTop = DEF(X, T) --> ( + topology(X, T) /\ + ∀(A, clopen(X, T, A) ==> ((A === emptySet) \/ (A === X))) + ) + + /** + * Intermediate value theorem + * + * The image of a connected space by a continuous, surjective mapping is a connected space + */ + val intermediateValueThm = Theorem((connectedTop(X, T1), continuous(f, X, T1, Y, T2), surjective(f, X, Y)) |- connectedTop(Y, T2)) { + assume(connectedTop(X, T1), continuous(f, X, T1, Y, T2), surjective(f, X, Y)) + val xIsTop = have(topology(X, T1)) by Tautology.from(continuous.definition, mapping.definition) + val yIsTop = have(topology(Y, T2)) by Tautology.from(continuous.definition, mapping.definition) + + val xIsConnected = have(∀(A, clopen(X, T1, A) ==> ((A === emptySet) \/ (A === X)))) by Tautology.from(connectedTop.definition of (T := T1)) + val isContinuous = have(∀(O, O ∈ T2 ==> preimage(f, X, Y, O) ∈ T1)) by Tautology.from(continuous.definition) + + val fIsFunction = have(functionFrom(f, X, Y)) by Tautology.from(continuous.definition, mapping.definition) + + have(clopen(Y, T2, A) ==> ((A === emptySet) \/ (A === Y))) subproof { + assume(clopen(Y, T2, A)) + + val aIsSubset = have(A ⊆ Y) subproof { + have(A ∈ T2) by Tautology.from(clopen.definition of (X := Y, T := T2)) + have(A ∈ powerSet(Y)) by Tautology.from( + lastStep, + yIsTop, + topology.definition of (X := Y, T := T2), + setOfSubsets.definition of (X := Y, T := T2), + subsetTactic of (x := T2, y := powerSet(Y), z := A) + ) + have(thesis) by Tautology.from(lastStep, powerAxiom of (x := A, y := Y)) + } + + val preimageA = have(A ∈ T2 ==> preimage(f, X, Y, A) ∈ T1) by InstantiateForall(A)(isContinuous) + val yIsClopen = have(A ∈ T2 /\ setDifference(Y, A) ∈ T2) by Tautology.from(clopen.definition of (X := Y, T := T2)) + val part1 = have(preimage(f, X, Y, A) ∈ T1) by Tautology.from(yIsClopen, preimageA) + val preimageYA = have(setDifference(Y, A) ∈ T2 ==> preimage(f, X, Y, setDifference(Y, A)) ∈ T1) by InstantiateForall(setDifference(Y, A))(isContinuous) + have(preimage(f, X, Y, setDifference(Y, A)) ∈ T1) by Tautology.from(yIsClopen, preimageYA) + val part2 = have(setDifference(X, preimage(f, X, Y, A)) ∈ T1) by Tautology.from( + lastStep, + aIsSubset, + fIsFunction, + preimageDifference, + replaceEqualityContainsLeft of (x := setDifference(X, preimage(f, X, Y, A)), y := preimage(f, X, Y, setDifference(Y, A)), z := T1) + ) + + // So f^-1(A) is clopen + val inverseIsClopen = have(clopen(X, T1, preimage(f, X, Y, A))) by Tautology.from( + xIsTop, + part1, + part2, + clopen.definition of (T := T1, A := preimage(f, X, Y, A)) + ) + + // Hence (f^-1(A) === emptySet) \/ (preimage(f, X, Y, A) === X) by connectedness of X + have(clopen(X, T1, preimage(f, X, Y, A)) ==> (preimage(f, X, Y, A) === emptySet) \/ (preimage(f, X, Y, A) === X)) by InstantiateForall(preimage(f, X, Y, A))(xIsConnected) + val preImageIsConnected = have((preimage(f, X, Y, A) === emptySet) \/ (preimage(f, X, Y, A) === X)) by Tautology.from( + lastStep, + inverseIsClopen + ) + + // Use the fact that f(emptyset)=emptyset, f(f^-1(A)) = A (by surjectivity), f(X) = Y (by surjectivity) to conclude + val firstCase = have(preimage(f, X, Y, A) === emptySet |- A === emptySet) subproof { + assume(preimage(f, X, Y, A) === emptySet) + have(thesis) by Tautology.from( + lastStep, + fIsFunction, + aIsSubset, + applyDirectImage of (A := preimage(f, X, Y, A), B := emptySet), + directImagePreimageSurjective, + directImageEmptySet, + equalityTransitivity of (x := directImage(f, X, Y, preimage(f, X, Y, A)), y := directImage(f, X, Y, emptySet), z := emptySet), + equalitySymmetry of (x := directImage(f, X, Y, preimage(f, X, Y, A)), y := A), + equalityTransitivity of (x := A, y := directImage(f, X, Y, preimage(f, X, Y, A)), z := emptySet) + ) + } + + val secondCase = have(preimage(f, X, Y, A) === X |- A === Y) subproof { + assume(preimage(f, X, Y, A) === X) + have(thesis) by Tautology.from( + lastStep, + fIsFunction, + aIsSubset, + applyDirectImage of (A := preimage(f, X, Y, A), B := X), + directImagePreimageSurjective, + directImageX, + surjectiveImpliesRangeIsCodomain of (x := X, y := Y), + equalitySymmetry of (x := Y, y := functionRange(f)), + equalityTransitivity of (x := directImage(f, X, Y, X), y := functionRange(f), z := Y), + equalityTransitivity of (x := directImage(f, X, Y, preimage(f, X, Y, A)), y := directImage(f, X, Y, X), z := Y), + equalitySymmetry of (x := directImage(f, X, Y, preimage(f, X, Y, A)), y := A), + equalityTransitivity of (x := A, y := directImage(f, X, Y, preimage(f, X, Y, A)), z := Y) + ) + } + + have(thesis) by Tautology.from(preImageIsConnected, firstCase, secondCase) + } + + val allClopen = thenHave(∀(A, clopen(Y, T2, A) ==> ((A === emptySet) \/ (A === Y)))) by RightForall + have(connectedTop(Y, T2)) by Tautology.from(allClopen, yIsTop, connectedTop.definition of (X := Y, T := T2)) + } +} diff --git a/lisa-topology/src/main/scala/lisa/maths/topology/DiscreteTopology.scala b/lisa-topology/src/main/scala/lisa/maths/topology/DiscreteTopology.scala new file mode 100644 index 000000000..fba614a79 --- /dev/null +++ b/lisa-topology/src/main/scala/lisa/maths/topology/DiscreteTopology.scala @@ -0,0 +1,180 @@ +package lisa.maths.topology + +import lisa.automation.settheory.SetTheoryTactics.* +import lisa.maths.Quantifiers.* + +import lisa.automation.kernel.CommonTactics.Definition + +import lisa.maths.topology.Topology.* +import lisa.maths.settheory.* +import lisa.maths.settheory.SetTheory.* +import lisa.maths.settheory.SetTheoryBasics.* +import lisa.automation.kernel.CommonTactics.* + +object DiscreteTopology extends lisa.Main { + import lisa.maths.settheory.SetTheory.* + // var defs + private val x, y, z, a, b, c, t = variable + private val X, T = variable + private val A, B, Y = variable + + // A discrete Topology is is where T contains all possible subsets of X from Def 1.1.6 in the book + val discreteTopology = DEF(X, T) --> nonEmpty(X) /\ (T === powerSet(X)) + + // Proof that a discrite Topology is actually a topology (satisfies all conditions of a topology) + val discreteIsTopology = Theorem( + discreteTopology(X, T) |- topology(X, T) + ) { + assume(discreteTopology(X, T)) + val discreteDef = have(nonEmpty(X) /\ (T === powerSet(X))) by Tautology.from(discreteTopology.definition) + val ext = have(forall(z, in(z, T) <=> in(z, powerSet(X)))) by Tautology.from(extensionalityAxiom of (x := T, y := powerSet(X)), discreteDef) + + val isSub = have(setOfSubsets(X, T)) by Tautology.from(equalityBySubset of (x := T, y := powerSet(X)), discreteDef, setOfSubsets.definition) + val contEx = have(containsExtremes(X, T)) subproof { + val a1 = have(in(∅, T) <=> in(∅, powerSet(X))) by InstantiateForall(∅)(ext) + val a2 = have(∅ ∈ powerSet(X)) by Tautology.from(powerAxiom of (x := ∅, y := X), emptySetIsASubset of (x := X)) + val hasEmpty = have(∅ ∈ T) by Tautology.from(a1, a2) + + have(in(X, T) <=> in(X, powerSet(X))) by InstantiateForall(X)(ext) + have(X ∈ T) by Tautology.from(lastStep, elemInItsPowerSet of (x := X)) + have(thesis) by Tautology.from(lastStep, hasEmpty, containsExtremes.definition) + } + val contUn = have(containsUnion(T)) subproof { + have((Y ⊆ T) |- (union(Y) ∈ T)) subproof { + assume(Y ⊆ T) + have(Y ⊆ powerSet(X)) by Tautology.from(discreteDef, equalityBySubset of (x := T, y := powerSet(X)), subsetTransitivity of (a := Y, b := T, c := powerSet(X))) + have(union(Y) ∈ powerSet(X)) by Tautology.from(lastStep, subsetClosedUnion of (x := Y, y := X), powerAxiom of (x := union(Y), y := X)) + have(thesis) by Tautology.from(lastStep, discreteDef, replaceEqualityContainsRight of (x := T, y := powerSet(X), z := union(Y))) + } + thenHave((Y ⊆ T) ==> (union(Y) ∈ T)) by Tautology + thenHave(forall(Y, (Y ⊆ T) ==> (union(Y) ∈ T))) by RightForall + have(thesis) by Tautology.from(lastStep, containsUnion.definition) + } + val contInt = have(containsIntersection(T)) subproof { + have((A ∈ T, B ∈ T) |- (A ∩ B ∈ T)) subproof { + assume((A ∈ T), (B ∈ T)) + val first = have(A ⊆ X) by Tautology.from(discreteDef, replaceEqualityContainsRight of (x := T, y := powerSet(X), z := A), powerAxiom of (x := A, y := X)) + val second = have(B ⊆ X) by Tautology.from(discreteDef, replaceEqualityContainsRight of (x := T, y := powerSet(X), z := B), powerAxiom of (x := B, y := X)) + have(A ∩ B ∈ powerSet(X)) by Tautology.from(first, second, subsetClosedIntersection of (x := A, y := B, z := X), powerAxiom of (x := A ∩ B, y := X)) + have(thesis) by Tautology.from(lastStep, discreteDef, replaceEqualityContainsRight of (x := T, y := powerSet(X), z := A ∩ B)) + } + have((A ∈ T /\ B ∈ T) ==> (A ∩ B ∈ T)) by Tautology.from(lastStep, containsIntersection.definition) + thenHave(forall(B, (A ∈ T /\ B ∈ T) ==> (A ∩ B ∈ T))) by RightForall + thenHave(forall(A, forall(B, (A ∈ T /\ B ∈ T) ==> (A ∩ B ∈ T)))) by RightForall + have(thesis) by Tautology.from(lastStep, containsIntersection.definition) + } + + have(thesis) by Tautology.from(discreteDef, isSub, contEx, contUn, contInt, topology.definition) + } + + // A indiscrete Topology is is where T contains only the empty set and X. Therefore the smallest possible topology for a given X. From Def 1.1.6 in the book + val indiscreteTopology = DEF(X, T) --> nonEmpty(X) /\ (T === unorderedPair(∅, X)) + + // proof that the indiscrete Topology is acutally a topology + val indiscreteIsTopology = Theorem( + indiscreteTopology(X, T) ==> topology(X, T) + ) { + assume(indiscreteTopology(X, T)) + val indiscreteDef = have(nonEmpty(X) /\ (T === unorderedPair(∅, X))) by Tautology.from(indiscreteTopology.definition) + val emptySubs = have(∅ ∈ powerSet(X)) by Tautology.from(emptySetIsASubset of (x := X), powerAxiom of (x := emptySet, y := X)) + val fullSubs = have(X ∈ powerSet(X)) by Tautology.from(elemInItsPowerSet of (x := X)) + + val isSub = have(setOfSubsets(X, T)) subproof { + have(in(unorderedPair(∅, X), powerSet(powerSet(X)))) by Tautology.from(emptySubs, fullSubs, unorderedPairInPowerSet of (x := powerSet(X), a := emptySet, b := X)) + have(unorderedPair(∅, X) ⊆ powerSet(X)) by Tautology.from(lastStep, powerAxiom of (x := unorderedPair(∅, X), y := powerSet(X))) + have(thesis) by Tautology.from(lastStep, indiscreteDef, replaceEqualitySubsetLeft of (x := unorderedPair(∅, X), y := T, z := powerSet(X)), setOfSubsets.definition) + } + + val contEx = have(containsExtremes(X, T)) subproof { + val a = have(X ∈ T) by Tautology.from(pairAxiom of (x := emptySet, y := X, z := X), indiscreteDef, replaceEqualityContainsRight of (x := T, y := unorderedPair(∅, X), z := X)) + val b = have(∅ ∈ T) by Tautology.from( + pairAxiom of (x := emptySet, y := X, z := emptySet), + indiscreteDef, + replaceEqualityContainsRight of (x := T, y := unorderedPair(∅, X), z := emptySet) + ) + have(thesis) by Tautology.from(a, b, containsExtremes.definition) + } + + val contUn = have(containsUnion(T)) subproof { + have((Y ⊆ T) |- union(Y) ∈ T) subproof { + assume(Y ⊆ T) + have(Y ⊆ unorderedPair(∅, X)) by Tautology.from(indiscreteDef, replaceEqualitySubsetRight of (x := T, y := unorderedPair(∅, X), z := Y)) + have(forall(z, in(z, Y) ==> in(z, unorderedPair(∅, X)))) by Tautology.from(lastStep, subsetAxiom of (x := Y, y := unorderedPair(∅, X))) + thenHave(in(z, Y) ==> in(z, unorderedPair(∅, X))) by InstantiateForall(z) + have(in(z, Y) |- ((z === ∅) \/ (z === X))) by Tautology.from(lastStep, pairAxiom of (x := emptySet, y := X)) + thenHave((in(z, Y) /\ in(a, z)) |- (((z === ∅) \/ (z === X)) /\ in(a, z))) by Tautology + thenHave((in(z, Y) /\ in(a, z)) |- ((((z === ∅) /\ in(a, z))) \/ ((z === X) /\ in(a, z)))) by Tautology + have((in(z, Y) /\ in(a, z)) |- (in(a, ∅) \/ (in(a, X) /\ (z === X)))) by Tautology.from( + lastStep, + replaceEqualityContainsRight of (x := z, y := emptySet, z := a), + replaceEqualityContainsRight of (x := z, y := X, z := a) + ) + have((in(z, Y) /\ in(a, z)) |- (in(a, X) /\ (z === X) /\ in(z, Y))) by Tautology.from(lastStep, emptySetAxiom of (x := a)) + have((in(z, Y) /\ in(a, z)) |- (in(a, X) /\ in(X, Y))) by Tautology.from(lastStep, replaceEqualityContainsLeft of (x := z, y := X, z := Y)) + thenHave(exists(z, in(z, Y) /\ in(a, z)) |- (in(a, X) /\ in(X, Y))) by LeftExists + val before = have(in(a, union(Y)) ==> (in(a, X) /\ in(X, Y))) by Tautology.from(lastStep, unionAxiom of (z := a, x := Y, y := z), emptySetAxiom of (x := a)) + thenHave(in(a, union(Y)) ==> in(a, X)) by Tautology + val base = thenHave(forall(a, in(a, union(Y)) ==> in(a, X))) by RightForall + val cond1 = have(forall(a, !in(a, union(Y))) |- union(Y) === ∅) by Tautology.from(setWithNoElementsIsEmpty of (y := a, x := union(Y))) + val cond2 = have(exists(a, in(a, union(Y))) |- union(Y) === X) subproof { + val unionGrow = have(in(a, union(Y)) |- (X ⊆ union(Y))) by Tautology.from(before, unionDoesntShrink of (x := X, y := Y)) + have(in(a, union(Y)) |- (union(Y) === X)) by Tautology.from(base, unionGrow, subsetAxiom of (x := union(Y), y := X, z := a), equalityBySubset of (x := union(Y), y := X)) + thenHave(thesis) by LeftExists + } + have((union(Y) === ∅) \/ (union(Y) === X)) by Tautology.from(base, cond1, cond2) + have(union(Y) ∈ unorderedPair(∅, X)) by Tautology.from(lastStep, pairAxiom of (x := emptySet, y := X, z := union(Y))) + have(thesis) by Tautology.from(lastStep, indiscreteDef, replaceEqualityContainsRight of (x := unorderedPair(∅, X), y := T, z := union(Y))) + } + thenHave((Y ⊆ T) ==> (union(Y) ∈ T)) by Tautology + thenHave(forall(Y, (Y ⊆ T) ==> (union(Y) ∈ T))) by RightForall + have(thesis) by Tautology.from(lastStep, containsUnion.definition) + } + + val contInt = have(containsIntersection(T)) subproof { + have((A ∈ T /\ B ∈ T) |- (A ∩ B ∈ T)) subproof { + assume((A ∈ T /\ B ∈ T)) + have(A ∈ unorderedPair(∅, X) /\ B ∈ unorderedPair(∅, X)) by Tautology.from( + indiscreteDef, + replaceEqualityContainsRight of (x := T, y := unorderedPair(∅, X), z := A), + replaceEqualityContainsRight of (x := T, y := unorderedPair(∅, X), z := B) + ) + val allPossibilities = + have(((A === ∅) \/ (A === X)) /\ ((B === ∅) \/ (B === X))) by Tautology.from(lastStep, pairAxiom of (x := emptySet, y := X, z := A), pairAxiom of (x := emptySet, y := X, z := B)) + val aEmpty = have((A === ∅) |- (A ∩ B) === ∅) subproof { + assume(A === emptySet) + have(in(t, setIntersection(A, B)) <=> (in(t, A) /\ in(t, B))) by Tautology.from(setIntersectionMembership of (x := A, y := B)) + have(!in(t, setIntersection(A, B))) by Tautology.from(lastStep, replaceEqualityContainsRight of (x := emptySet, y := A, z := t), emptySetAxiom of (x := t)) + thenHave(forall(t, !in(t, setIntersection(A, B)))) by RightForall + have(thesis) by Tautology.from(lastStep, setWithNoElementsIsEmpty of (y := t, x := setIntersection(A, B))) + } + val oneEmpty = have(((A === ∅) \/ (B === ∅)) |- ((A ∩ B) === ∅)) by Tautology.from( + aEmpty, + aEmpty of (A := B, B := A), + setIntersectionCommutativity of (x := A, y := B), + equalityTransitivity of (x := setIntersection(A, B), y := setIntersection(B, A), z := emptySet) + ) + val bothFull = have((A === X, B === X) |- A ∩ B === X) subproof { + assume(((A === X) /\ (B === X))) + have(in(t, setIntersection(A, B)) <=> (in(t, A) /\ in(t, B))) by Tautology.from(setIntersectionMembership of (x := A, y := B)) + have(in(t, setIntersection(A, B)) <=> in(t, X)) by Tautology.from( + lastStep, + replaceEqualityContainsRight of (x := X, y := A, z := t), + replaceEqualityContainsRight of (x := X, y := B, z := t) + ) + thenHave(forall(t, in(t, setIntersection(A, B)) <=> in(t, X))) by RightForall + have(thesis) by Tautology.from(lastStep, extensionalityAxiom of (x := setIntersection(A, B), y := X, z := t)) + } + have((A ∩ B === ∅) \/ (A ∩ B === X)) by Tautology.from(allPossibilities, oneEmpty, bothFull) + have(in(A ∩ B, unorderedPair(∅, X))) by Tautology.from(lastStep, pairAxiom of (z := setIntersection(A, B), x := emptySet, y := X)) + have(thesis) by Tautology.from(lastStep, indiscreteDef, replaceEqualityContainsRight of (x := unorderedPair(∅, X), y := T, z := setIntersection(A, B))) + } + thenHave((A ∈ T /\ B ∈ T) ==> A ∩ B ∈ T) by Tautology + thenHave(forall(B, (A ∈ T /\ B ∈ T) ==> A ∩ B ∈ T)) by RightForall + thenHave(forall(A, forall(B, (A ∈ T /\ B ∈ T) ==> A ∩ B ∈ T))) by RightForall + have(thesis) by Tautology.from(lastStep, containsIntersection.definition) + } + + have(thesis) by Tautology.from(indiscreteDef, isSub, contEx, contUn, contInt, topology.definition) + } + +} diff --git a/lisa-topology/src/main/scala/lisa/maths/topology/Intersection.scala b/lisa-topology/src/main/scala/lisa/maths/topology/Intersection.scala new file mode 100644 index 000000000..dd8a348a2 --- /dev/null +++ b/lisa-topology/src/main/scala/lisa/maths/topology/Intersection.scala @@ -0,0 +1,94 @@ +package lisa.maths.topology + +import lisa.automation.settheory.SetTheoryTactics.* +import lisa.maths.Quantifiers.* + +import lisa.automation.kernel.CommonTactics.Definition + +import lisa.maths.topology.Topology.* +import lisa.maths.settheory.* +import lisa.maths.settheory.SetTheory.* +import lisa.maths.settheory.SetTheoryBasics.* + +object Intersection extends lisa.Main { + // var defs + private val x, y, z, a, b, c, t, p = variable + private val X, T, T1, T2 = variable + private val S, A, B, Y = variable + + // Proof that the intersection over two topologies defined over the same set X is also a topology + val intersectionIsTopology = Theorem( + (topology(X, T1) /\ topology(X, T2)) |- topology(X, T1 ∩ T2) + ) { + assume(topology(X, T1) /\ topology(X, T2)) + val topo1 = have(nonEmpty(X) /\ setOfSubsets(X, T1) /\ containsExtremes(X, T1) /\ containsUnion(T1) /\ containsIntersection(T1)) by Tautology.from(topology.definition of (T := T1)) + val topo2 = have(nonEmpty(X) /\ setOfSubsets(X, T2) /\ containsExtremes(X, T2) /\ containsUnion(T2) /\ containsIntersection(T2)) by Tautology.from(topology.definition of (T := T2)) + + val nonEm = have(nonEmpty(X)) by Tautology.from(topo1) + + val isSub = have(setOfSubsets(X, T1 ∩ T2)) by Tautology.from( + subsetClosedIntersection of (x := T1, y := T2, z := powerSet(X)), + topo1, + topo2, + setOfSubsets.definition of (T := T1 ∩ T2), + setOfSubsets.definition of (T := T1), + setOfSubsets.definition of (T := T2) + ) + val contEx = have(containsExtremes(X, T1 ∩ T2)) subproof { + val empty = have(∅ ∈ (T1 ∩ T2)) by Tautology.from( + setIntersectionMembership of (t := emptySet, x := T1, y := T2), + containsExtremes.definition of (T := T1), + containsExtremes.definition of (T := T2), + topo1, + topo2 + ) + val full = have(X ∈ (T1 ∩ T2)) by Tautology.from( + setIntersectionMembership of (t := X, x := T1, y := T2), + containsExtremes.definition of (T := T1), + containsExtremes.definition of (T := T2), + topo1, + topo2 + ) + have(thesis) by Tautology.from(empty, full, containsExtremes.definition of (T := T1 ∩ T2)) + } + val contUn = have(containsUnion(T1 ∩ T2)) subproof { + have(forall(Y, (Y ⊆ T1) ==> (union(Y) ∈ T1))) by Tautology.from(topo1, containsUnion.definition of (T := T1)) + val t1 = thenHave((Y ⊆ T1) ==> (union(Y) ∈ T1)) by InstantiateForall(Y) + have(forall(Y, (Y ⊆ T2) ==> (union(Y) ∈ T2))) by Tautology.from(topo2, containsUnion.definition of (T := T2)) + val t2 = thenHave((Y ⊆ T2) ==> (union(Y) ∈ T2)) by InstantiateForall(Y) + have((Y ⊆ (T1 ∩ T2)) ==> (union(Y) ∈ (T1 ∩ T2))) subproof { + assume(Y ⊆ (T1 ∩ T2)) + val leadsUnion = have((containsUnion(T), Y ⊆ T) |- union(Y) ∈ T) subproof { + assume(containsUnion(T)) + have(forall(Y, (Y ⊆ T) ==> (union(Y) ∈ T))) by Tautology.from(containsUnion.definition) + thenHave((Y ⊆ T) ==> (union(Y) ∈ T)) by InstantiateForall(Y) + thenHave(thesis) by Tautology + } + have((Y ⊆ T1) /\ (Y ⊆ T2)) by Tautology.from(subsetUnderIntersection of (x := T1, y := T2, z := Y)) + have(union(Y) ∈ T1 /\ union(Y) ∈ T2) by Tautology.from(leadsUnion of (T := T1), leadsUnion of (T := T2), lastStep, topo1, topo2) + have(thesis) by Tautology.from(lastStep, setIntersectionMembership of (x := T1, y := T2, t := union(Y))) + } + thenHave(forall(Y, (Y ⊆ (T1 ∩ T2)) ==> (union(Y) ∈ (T1 ∩ T2)))) by RightForall + have(thesis) by Tautology.from(lastStep, containsUnion.definition of (T := T1 ∩ T2)) + } + val contInt = have(containsIntersection(T1 ∩ T2)) subproof { + have((A ∈ (T1 ∩ T2) /\ B ∈ (T1 ∩ T2)) ==> A ∩ B ∈ (T1 ∩ T2)) subproof { + assume(A ∈ (T1 ∩ T2) /\ B ∈ (T1 ∩ T2)) + val leadsInt = have((containsIntersection(T), (A ∈ T /\ B ∈ T)) |- (A ∩ B ∈ T)) subproof { + assume(containsIntersection(T)) + have(forall(A, forall(B, (A ∈ T /\ B ∈ T) ==> A ∩ B ∈ T))) by Tautology.from(containsIntersection.definition) + thenHave(forall(B, (A ∈ T /\ B ∈ T) ==> A ∩ B ∈ T)) by InstantiateForall(A) + thenHave((A ∈ T /\ B ∈ T) ==> A ∩ B ∈ T) by InstantiateForall(B) + thenHave(thesis) by Tautology + } + have(A ∈ T1 /\ A ∈ T2 /\ B ∈ T1 /\ B ∈ T2) by Tautology.from(setIntersectionMembership of (t := A, x := T1, y := T2), setIntersectionMembership of (t := B, x := T1, y := T2)) + have(A ∩ B ∈ T1 /\ A ∩ B ∈ T2) by Tautology.from(lastStep, leadsInt of (T := T1), leadsInt of (T := T2), topo1, topo2) + have(thesis) by Tautology.from(lastStep, setIntersectionMembership of (t := A ∩ B, x := T1, y := T2)) + } + thenHave(forall(B, (A ∈ (T1 ∩ T2) /\ B ∈ (T1 ∩ T2)) ==> A ∩ B ∈ (T1 ∩ T2))) by RightForall + thenHave(forall(A, forall(B, (A ∈ (T1 ∩ T2) /\ B ∈ (T1 ∩ T2)) ==> A ∩ B ∈ (T1 ∩ T2)))) by RightForall + have(thesis) by Tautology.from(lastStep, containsIntersection.definition of (T := T1 ∩ T2)) + } + have(thesis) by Tautology.from(nonEm, isSub, contEx, contUn, contInt, topology.definition of (T := T1 ∩ T2)) + } +} diff --git a/lisa-topology/src/main/scala/lisa/maths/topology/SingletonSet.scala b/lisa-topology/src/main/scala/lisa/maths/topology/SingletonSet.scala new file mode 100644 index 000000000..6e44a9ac4 --- /dev/null +++ b/lisa-topology/src/main/scala/lisa/maths/topology/SingletonSet.scala @@ -0,0 +1,254 @@ +package lisa.maths.topology + +import lisa.automation.settheory.SetTheoryTactics.* +import lisa.maths.Quantifiers.* + +import lisa.automation.kernel.CommonTactics.Definition + +import lisa.maths.topology.DiscreteTopology.* +import lisa.maths.topology.Topology.* +import lisa.maths.settheory.* +import lisa.maths.settheory.SetTheory.* +import lisa.maths.settheory.SetTheoryBasics.* +import lisa.automation.kernel.CommonTactics.* +import lisa.maths.settheory.functions.Functionals.* +import lisa.automation.settheory.SetTheoryTactics.UniqueComprehension +import lisa.automation.settheory.SetTheoryTactics.TheConditional + +object SingletonSet extends lisa.Main { + import lisa.maths.settheory.SetTheory.* + // var defs + private val x, y, z, a, b, c, t, p, f, s = variable + private val X, T = variable + private val S, A, B, Y = variable + + /* + Theorem: singletonSets exists and it is unique + exists unique set z whose members are {x} for each x in S + */ + val singletonSetsUniqueness = Theorem( + ∃!(z, ∀(t, in(t, z) <=> exists(x, in(x, S) /\ (t === singleton(x))))) + ) { + // prove that {x} for each x in S is member of U(SxS) + val implicationProof = have(exists(x, in(x, S) /\ (t === singleton(x))) ==> in(t, union(cartesianProduct(S, S)))) subproof { + + val elementInSingleton = have(in(x, singleton(x))) subproof { + have(thesis) by Tautology.from(pairAxiom of (x := x, y := x, z := x)) + } + + val singletonInPowerSet = have(in(x, S) |- in(singleton(x), powerSet(S))) subproof { + assume(in(x, S)) + thenHave((x === y) |- in(y, S)) by Substitution.ApplyRules(x === y) + have(in(y, singleton(x)) |- in(y, S)) by Tautology.from(lastStep, singletonHasNoExtraElements) + thenHave(() |- (!(in(y, singleton(x))), in(y, S))) by RightNot + thenHave(() |- in(y, singleton(x)) ==> in(y, S)) by Tautology + thenHave(() |- forall(y, in(y, singleton(x)) ==> in(y, S))) by RightForall + have(() |- singleton(x) ⊆ S) by Tautology.from(lastStep, subsetAxiom of (z := y, y := S, x := singleton(x))) + have(thesis) by Tautology.from(lastStep, powerAxiom of (x := singleton(x), y := S)) + } + + val abExist = have((singleton(t) === pair(x, x)) /\ in(x, S) |- ∃(a, ∃(b, (singleton(t) === pair(a, b)) /\ in(a, S) /\ in(b, S)))) subproof { + have((singleton(t) === pair(x, x)) /\ in(x, S) |- (singleton(t) === pair(x, x)) /\ in(x, S) /\ in(x, S)) by Restate + thenHave((singleton(t) === pair(x, x)) /\ in(x, S) |- exists(b, (singleton(t) === pair(x, b)) /\ in(x, S) /\ in(b, S))) by RightExists + thenHave((singleton(t) === pair(x, x)) /\ in(x, S) |- exists(a, exists(b, (singleton(t) === pair(a, b)) /\ in(a, S) /\ in(b, S)))) by RightExists + } + + // replace the cartesianProduct with its definitions using powerSet and setUnion + val cartesianInstantiated = have( + in(singleton(t), cartesianProduct(S, S)) <=> (in(singleton(t), powerSet(powerSet(setUnion(S, S)))) + /\ ∃(a, ∃(b, (singleton(t) === pair(a, b)) /\ in(a, S) /\ in(b, S)))) + ) subproof { + val instance = have( + (cartesianProduct(x, y) === cartesianProduct(x, y)) <=> ∀( + t, + in(t, cartesianProduct(x, y)) <=> (in(t, powerSet(powerSet(setUnion(x, y)))) + /\ ∃(a, ∃(b, (t === pair(a, b)) /\ in(a, x) /\ in(b, y)))) + ) + ) by InstantiateForall(cartesianProduct(x, y))(cartesianProduct.definition) + thenHave( + ∀( + t, + in(t, cartesianProduct(x, y)) <=> (in(t, powerSet(powerSet(setUnion(x, y)))) + /\ ∃(a, ∃(b, (t === pair(a, b)) /\ in(a, x) /\ in(b, y)))) + ) + ) by Tautology + thenHave( + in(singleton(t), cartesianProduct(x, y)) <=> (in(singleton(t), powerSet(powerSet(setUnion(x, y)))) + /\ ∃(a, ∃(b, (singleton(t) === pair(a, b)) /\ in(a, x) /\ in(b, y)))) + ) by InstantiateForall(singleton(t)) + thenHave( + forall( + x, + in(singleton(t), cartesianProduct(x, y)) <=> (in(singleton(t), powerSet(powerSet(setUnion(x, y)))) + /\ ∃(a, ∃(b, (singleton(t) === pair(a, b)) /\ in(a, x) /\ in(b, y)))) + ) + ) by RightForall + thenHave( + in(singleton(t), cartesianProduct(S, y)) <=> (in(singleton(t), powerSet(powerSet(setUnion(S, y)))) + /\ ∃(a, ∃(b, (singleton(t) === pair(a, b)) /\ in(a, S) /\ in(b, y)))) + ) by InstantiateForall(S) + thenHave( + forall( + y, + in(singleton(t), cartesianProduct(S, y)) <=> (in(singleton(t), powerSet(powerSet(setUnion(S, y)))) + /\ ∃(a, ∃(b, (singleton(t) === pair(a, b)) /\ in(a, S) /\ in(b, y)))) + ) + ) by RightForall + thenHave( + in(singleton(t), cartesianProduct(S, S)) <=> (in(singleton(t), powerSet(powerSet(setUnion(S, S)))) + /\ ∃(a, ∃(b, (singleton(t) === pair(a, b)) /\ in(a, S) /\ in(b, S)))) + ) by InstantiateForall(S) + } + + have(in(x, S) |- in(x, S)) by Restate + have(in(x, S) |- in(x, setUnion(S, S))) by Tautology.from(lastStep, setUnionMembership of (z := x, x := S, y := S)) + have(in(x, S) |- in(singleton(x), powerSet(setUnion(S, S))) /\ (singleton(singleton(x)) === pair(x, x))) by + Tautology.from(lastStep, singletonInPowerSet of (S := setUnion(S, S))) + thenHave((in(x, S), t === singleton(x)) |- in(t, powerSet(setUnion(S, S))) /\ (singleton(t) === pair(x, x))) by + Substitution.ApplyRules(singleton(x) === t) + thenHave(in(x, S) /\ (t === singleton(x)) |- in(t, powerSet(setUnion(S, S))) /\ (singleton(t) === pair(x, x))) by Tautology + have(in(x, S) /\ (t === singleton(x)) |- in(singleton(t), powerSet(powerSet(setUnion(S, S)))) /\ (singleton(t) === pair(x, x))) by + Tautology.from(lastStep, singletonInPowerSet of (x := t, S := powerSet(setUnion(S, S)))) + have( + in(x, S) /\ (t === singleton(x)) |- in(singleton(t), powerSet(powerSet(setUnion(S, S)))) /\ in(t, singleton(t)) + /\ ((singleton(t) === pair(x, x)) /\ in(x, S)) + ) by Tautology.from(lastStep, elementInSingleton of (x := t)) + have( + in(x, S) /\ (t === singleton(x)) |- in(singleton(t), powerSet(powerSet(setUnion(S, S)))) /\ in(t, singleton(t)) + /\ ∃(a, ∃(b, (singleton(t) === pair(a, b)) /\ in(a, S) /\ in(b, S))) + ) by Tautology.from(lastStep, abExist) + have(in(x, S) /\ (t === singleton(x)) |- in(singleton(t), cartesianProduct(S, S)) /\ in(t, singleton(t))) by + Tautology.from(lastStep, cartesianInstantiated) + thenHave(in(x, S) /\ (t === singleton(x)) |- exists(z, in(z, cartesianProduct(S, S)) /\ in(t, z))) by RightExists + have((in(x, S) /\ (t === singleton(x))) |- in(t, union(cartesianProduct(S, S)))) by + Tautology.from(lastStep, unionAxiom of (y := z, x := cartesianProduct(S, S), z := t)) + thenHave(exists(x, (in(x, S) /\ (t === singleton(x)))) |- in(t, union(cartesianProduct(S, S)))) by LeftExists + } + + // use unique comprehension from original set U(SxS) with the provided predicate and the membership proof + have(() |- existsOne(z, forall(t, in(t, z) <=> exists(x, in(x, S) /\ (t === singleton(x)))))) by UniqueComprehension.fromOriginalSet( + union(cartesianProduct(S, S)), + lambda(t, exists(x, in(x, S) /\ (t === singleton(x)))), + implicationProof + ) + } + val singletonSets = DEF(S) --> The(z, ∀(t, in(t, z) <=> exists(x, in(x, S) /\ (t === singleton(x)))))(singletonSetsUniqueness) + + val singletonSetsMembershipRaw = Theorem( + in(t, singletonSets(S)) <=> exists(x, ((t === singleton(x)) /\ in(x, S))) + ) { + have(∀(t, in(t, singletonSets(S)) <=> exists(x, in(x, S) /\ (t === singleton(x))))) by InstantiateForall(singletonSets(S))(singletonSets.definition) + thenHave(thesis) by InstantiateForall(t) + } + + /* + Theorem: x is member of S iff {x} is member of singletonSets(S) + */ + val singletonSetsMembership = Theorem( + in(x, S) <=> in(singleton(x), singletonSets(S)) + ) { + val form = formulaVariable + val memb = have(in(t, singletonSets(S)) <=> exists(x, ((t === singleton(x)) /\ in(x, S)))) by Tautology.from(singletonSetsMembershipRaw) + val forward = have(in(x, S) |- in(singleton(x), singletonSets(S))) subproof { + assume(in(x, S)) + have(t === singleton(x) |- ((t === singleton(x)) /\ in(x, S))) by Tautology + thenHave(t === singleton(x) |- exists(x, ((t === singleton(x)) /\ in(x, S)))) by RightExists + have((t === singleton(x)) ==> in(t, singletonSets(S))) by Tautology.from(lastStep, memb) + thenHave(forall(t, (t === singleton(x)) ==> in(t, singletonSets(S)))) by RightForall + thenHave((singleton(x) === singleton(x)) ==> in(singleton(x), singletonSets(S))) by InstantiateForall(singleton(x)) + have(thesis) by Tautology.from(lastStep) + } + val backward = have(in(singleton(x), singletonSets(S)) |- in(x, S)) subproof { + assume(in(singleton(x), singletonSets(S))) + have(exists(y, ((singleton(x) === singleton(y)) /\ in(y, S))) |- in(x, S)) subproof { + have(((singleton(x) === singleton(y)) /\ in(y, S)) |- in(x, S)) by Tautology.from(replaceEqualityContainsLeft of (z := S), singletonExtensionality) + thenHave(thesis) by LeftExists + } + have(thesis) by Tautology.from(lastStep, singletonSetsMembershipRaw of (t := singleton(x), y := x)) + } + have(thesis) by Tautology.from(forward, backward) + } + + /* + Theorem: union of sinletonSets(S) is equivalent to S + */ + val unionSingletonSets = Theorem(union(singletonSets(S)) === S) { + + val elementInSingleton = have(in(x, singleton(x))) by Tautology.from(pairAxiom of (x := x, y := x, z := x)) + + // prove that all elements of the union of singletonSets(S) are in S + val fwd = have(in(x, union(singletonSets(S))) |- in(x, S)) subproof { + have(in(z, S) |- in(z, S)) by Restate + thenHave((in(z, S), (x === z)) |- in(x, S)) by Substitution.ApplyRules(x === z) + have((in(z, S), in(x, singleton(z))) |- in(x, S)) by Tautology.from(lastStep, singletonHasNoExtraElements of (y := x, x := z)) + thenHave((in(z, S), in(x, y), (y === singleton(z))) |- in(x, S)) by Substitution.ApplyRules(y === singleton(z)) + thenHave((in(z, S) /\ (y === singleton(z)), in(x, y)) |- in(x, S)) by Tautology + thenHave((exists(z, in(z, S) /\ (y === singleton(z))), in(x, y)) |- in(x, S)) by LeftExists + thenHave(exists(z, in(z, S) /\ (y === singleton(z))) /\ in(x, y) |- in(x, S)) by Tautology + have(in(y, singletonSets(S)) /\ in(x, y) |- in(x, S)) by Tautology.from(lastStep, singletonSetsMembershipRaw of (x := z, t := y)) + thenHave(exists(y, in(y, singletonSets(S)) /\ in(x, y)) |- in(x, S)) by LeftExists + have(thesis) by Tautology.from(lastStep, unionAxiom of (z := x, x := singletonSets(S))) + } + + // prove that all elements in S are in the union of singletonSets(S) + val bwd = have(in(x, S) |- in(x, union(singletonSets(S)))) subproof { + assume(in(x, S)) + have(in(x, S) /\ (singleton(x) === singleton(x))) by Restate + thenHave(exists(y, in(y, S) /\ (singleton(x) === singleton(y)))) by RightExists + have(in(singleton(x), singletonSets(S)) /\ in(x, singleton(x))) by + Tautology.from(lastStep, singletonSetsMembershipRaw of (x := y, t := singleton(x)), elementInSingleton) + thenHave(exists(y, in(y, singletonSets(S)) /\ in(x, y))) by RightExists + have(thesis) by Tautology.from(lastStep, unionAxiom of (z := x, x := singletonSets(S))) + } + + have(in(x, union(singletonSets(S))) <=> in(x, S)) by Tautology.from(fwd, bwd) + thenHave(forall(x, in(x, union(singletonSets(S))) <=> in(x, S))) by RightForall + have(thesis) by Tautology.from(lastStep, extensionalityAxiom of (z := x, x := union(singletonSets(S)), y := S)) + } + + /* + Theorem: a topology which contains all singleton sets of the elements of the ground set is the discrete one + */ + val ifContainsSingletonIsDiscrete = Theorem( + (topology(X, T), ∀(x, x ∈ X ==> singleton(x) ∈ T)) |- discreteTopology(X, T) + ) { + assume(∀(x, x ∈ X ==> singleton(x) ∈ T), topology(X, T)) + val topo = have(nonEmpty(X) /\ setOfSubsets(X, T) /\ containsExtremes(X, T) /\ containsUnion(T) /\ containsIntersection(T)) by Tautology.from(topology.definition) + have(forall(Y, (Y ⊆ T) ==> (union(Y) ∈ T))) by Tautology.from(topo, containsUnion.definition) + val contUnion = thenHave(singletonSets(S) ⊆ T ==> (union(singletonSets(S)) ∈ T)) by InstantiateForall(singletonSets(S)) + have(∀(x, x ∈ X ==> singleton(x) ∈ T)) by Tautology + val singleDef = thenHave((x ∈ X) ==> (singleton(x) ∈ T)) by InstantiateForall(x) + have(T === powerSet(X)) subproof { + // show T subs powerSet(X) (by def of topology) + val left = have(T ⊆ powerSet(X)) by Tautology.from(topo, setOfSubsets.definition) + // show powerSet(X) subs T + + // For any S ⊆ X we have S = U{x} -> S ∈ T by unionDef + have((S ⊆ X) |- S ∈ T) subproof { + assume(S ⊆ X) + have(forall(z, in(z, S) ==> in(z, X))) by Tautology.from(subsetAxiom of (x := S, y := X)) + thenHave(in(z, S) ==> in(z, X)) by InstantiateForall(z) + have(in(z, S) ==> in(singleton(z), T)) by Tautology.from(lastStep, singleDef of (x := z)) + have(in(singleton(z), singletonSets(S)) ==> in(singleton(z), T)) by Tautology.from(lastStep, singletonSetsMembership of (x := z)) + + have(((t === singleton(z)) /\ in(z, S)) |- in(t, singletonSets(S)) ==> in(t, T)) by Tautology.from( + lastStep, + replaceEqualityContainsLeft of (x := t, y := singleton(z), z := singletonSets(S)), + replaceEqualityContainsLeft of (x := t, y := singleton(z), z := T) + ) + thenHave(exists(z, (t === singleton(z)) /\ in(z, S)) |- in(t, singletonSets(S)) ==> in(t, T)) by LeftExists + have(in(t, singletonSets(S)) ==> in(t, T)) by Tautology.from(lastStep, singletonSetsMembershipRaw of (x := z)) + thenHave(forall(t, in(t, singletonSets(S)) ==> in(t, T))) by RightForall + have(singletonSets(S) ⊆ T) by Tautology.from(lastStep, subsetAxiom of (x := singletonSets(S), y := T)) + have(union(singletonSets(S)) ∈ T) by Tautology.from(lastStep, contUnion) + have(thesis) by Tautology.from(lastStep, unionSingletonSets, replaceEqualityContainsLeft of (x := union(singletonSets(S)), y := S, z := T)) + } + have(in(S, powerSet(X)) ==> in(S, T)) by Tautology.from(lastStep, powerAxiom of (x := S, y := X)) + thenHave(forall(S, in(S, powerSet(X)) ==> in(S, T))) by RightForall + val right = have(powerSet(X) ⊆ T) by Tautology.from(lastStep, subsetAxiom of (x := powerSet(X), y := T, z := S)) + + have(thesis) by Tautology.from(left, right, equalityBySubset of (x := powerSet(X), y := T)) + } + have(discreteTopology(X, T)) by Tautology.from(lastStep, topo, discreteTopology.definition) + } +} diff --git a/lisa-topology/src/main/scala/lisa/maths/topology/Topology.scala b/lisa-topology/src/main/scala/lisa/maths/topology/Topology.scala new file mode 100644 index 000000000..050ea9f3b --- /dev/null +++ b/lisa-topology/src/main/scala/lisa/maths/topology/Topology.scala @@ -0,0 +1,40 @@ +package lisa.maths.topology +import lisa.maths.settheory.* +import lisa.maths.settheory.SetTheory.* + +object Topology extends lisa.Main { + + private val X, T = variable + private val S, A, B, Y = variable + + /** + * The ground set X cannot be empty + */ + val nonEmpty = DEF(X) --> !(X === ∅) + + /** + * Elements of T are subsets of X + */ + val setOfSubsets = DEF(X, T) --> T ⊆ powerSet(X) + + /** + * X and the empty set ∅ belong to T + */ + val containsExtremes = DEF(X, T) --> ∅ ∈ T /\ X ∈ T + + /** + * The union of any (finite or infinite) number of sets in T belongs to T + */ + val containsUnion = DEF(T) --> forall(Y, (Y ⊆ T) ==> (union(Y) ∈ T)) + + /** + * The intersection of two sets in T belongs to T + */ + val containsIntersection = DEF(T) --> forall(A, forall(B, (A ∈ T /\ B ∈ T) ==> A ∩ B ∈ T)) + + /** + * By Definition 1.1.1 from the book the pair (X, T) is called a topological space. + * Or T is a topology on X + */ + val topology = DEF(X, T) --> nonEmpty(X) /\ setOfSubsets(X, T) /\ containsExtremes(X, T) /\ containsUnion(T) /\ containsIntersection(T) +} diff --git a/project/project/project/metals.sbt b/project/project/project/metals.sbt new file mode 100644 index 000000000..be029c0a4 --- /dev/null +++ b/project/project/project/metals.sbt @@ -0,0 +1,8 @@ +// format: off +// DO NOT EDIT! This file is auto-generated. + +// This file enables sbt-bloop to create bloop config files. + +addSbtPlugin("ch.epfl.scala" % "sbt-bloop" % "2.0.3") + +// format: on