Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
Download

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

31576 views
License: APACHE
Tweet
Share
Share
import data.set.basic

variables (R A : Type)
variables (𝕍 : set R β†’ set A) (𝕀 : set A β†’ set R)

open set

-- 𝕍 𝕀 𝕍 = 𝕍 for a contravariant Galois connection
-- for example the one between R=k[X₁,Xβ‚‚,…,Xβ‚™] and A=𝔸ⁿ
-- in the theory of algebraic varieties
example
  (𝕍_antimono : βˆ€ J₁ Jβ‚‚ : set R, J₁ βŠ† Jβ‚‚ β†’ 𝕍 Jβ‚‚ βŠ† 𝕍 J₁)
  (𝕀_antimono : βˆ€ W₁ Wβ‚‚ : set A, W₁ βŠ† Wβ‚‚ β†’ 𝕀 Wβ‚‚ βŠ† 𝕀 W₁)
  (galois : βˆ€ J : set R, βˆ€ W : set A, J βŠ† 𝕀 W ↔ W βŠ† 𝕍 J) :
  βˆ€ J : set R, 𝕍 (𝕀 (𝕍 J)) = 𝕍 J :=
begin
  intro J,
  apply set.subset.antisymm,
  { apply 𝕍_antimono,
    rw galois},
  { rw ←galois}
end