pedrominicz

module Universe where

-- http://blog.sigfpe.com/2006/12/evaluating-cellular-automata-is.html

import Control.Comonad

data Universe a = Universe [a] a [a] deriving (Eq, Show)

instance Functor Universe where
  fmap f (Universe ls x rs) = Universe (map f ls) (f x) (map f rs)

pedrominicz

import numpy as np
from qiskit import *
from qiskit.circuit.library import *

sim = Aer.get_backend('qasm_simulator')

# Create a quantum circuit with 2 qubits and 2 classical bits.
qc = QuantumCircuit(2, 2)

# Add a single-qubit Hadamard gate on qubit 0.

pedrominicz

import tactic

section

parameter {α : Type}

def r (a b : α × α) : Prop := a = b ∨ (a.snd, a.fst) = b

lemma r_refl : reflexive r :=
λ _, or.inl rfl

pedrominicz

import control.fix
import data.nat.upto

-- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Beautify.20code
-- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Fixing.20propositions

section

parameter {α : Type}

pedrominicz

import tactic

@[simp] def f (x : ℕ) : ℕ := x * 2

@[simp] def g (x : ℕ) : ℕ := x / 2

@[simp] lemma nat.mul_two_div_two (n : ℕ) : (n * 2) / 2 = n :=
by { induction n; simp }

#check nat.le_div_iff_mul_le

pedrominicz

-- https://plfa.github.io/Negation
-- https://www.youtube.com/watch?v=SJ-_zqw5UHk

-- A very interesting idea of the talk above is that there is no information in
-- a classical proposition. Note that `(p ↔ q) → p = q` imply that every
-- proposition is isomorphic to `true` or `false` and neither carry any
-- information. Constructive `or` and `exists` carry information, so `stable p`
-- and `stable q` imply `stable (p ∧ q)` but not `stable (p ∨ q)`.

section

pedrominicz

import topology.metric_space.basic
import topology.order

noncomputable theory

variables {α : Type*} [decidable_eq α]

@[simp] def dist' (x y : α) : ℝ := if x = y then 0 else 1

lemma eq_of_dist'_eq_zero (x y : α) : dist' x y = 0 → x = y :=

pedrominicz

import topology.order

variables {α : Type*}

namespace cofinite

@[simp] def is_open : set α → Prop :=
λ s, set.finite sᶜ ∨ s = ∅

lemma is_open_univ : is_open (set.univ : set α) :=

pedrominicz

import topology.algebra.ordered
import topology.metric_space.basic

-- Dê um exemplo de um espaço métrico `(X, d)` e uma família de subconjuntos
-- abertos `{Aᵢ | i ∈ I}` em `X`, tais que `⋂i ∈ I, Aᵢ` não é aberto.

-- Considere o espaço métrico `(X, d)` sendo `X = ℝ` e `d(x, y) := |x - y|`.

-- `f` é uma família infinita de conjuntos abertos em `ℝ` sendo
-- `fₙ := (-n⁻¹, n⁻¹)`.

pedrominicz

import data.real.basic data.real.cardinality data.set.disjointed
-- https://gist.github.com/pedrominicz/f03f3b5b405a08e2ba2c30529d5c2337
import .quotient_group_cardinality

-- https://www.youtube.com/watch?v=llnNaRzuvd4

open_locale big_operators

--def upper (f : ℕ → ennreal) : set ennreal :=
--  {a | ∀ n, ∑ (i : fin n), f i ≤ a}