Documentation

LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.InfLists

LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.InfLists #

Auxiliary declarations for the Borel determinacy formalization.

source
@[simp]
theorem Stream'.Discrete.append_inf_compose {A : Type u_1} (x y : List A) :
((fun (x_1 : Stream' A) => x ++ₛ x_1) ∘ fun (x : Stream' A) => y ++ₛ x) = fun (x_1 : Stream' A) => x ++ y ++ₛ x_1
source
@[simp]
theorem Stream'.Discrete.subAtInf_append {A : Type u_1} (T : Set (Stream' A)) (x y : List A) :
(fun (x : Stream' A) => y ++ₛ x) ⁻¹' (fun (x_1 : Stream' A) => x ++ₛ x_1) ⁻¹' T = (fun (x_1 : Stream' A) => x ++ y ++ₛ x_1) ⁻¹' T
source
def Stream'.Discrete.principalOpen {A : Type u_1} (x : List A) :
Set (Stream' A)

Auxiliary declaration for the Borel determinacy formalization.

Equations
Instances For
    source
    @[simp]
    theorem Stream'.Discrete.principalOpen_nil {A : Type u_1} :
    principalOpen [] = Set.univ
    source
    @[simp]
    theorem Stream'.Discrete.principalOpen_append {A : Type u_1} (a : Stream' A) (x y : List A) :
    x ++ₛ a ∈ principalOpen (x ++ y) ↔ a ∈ principalOpen y
    source
    @[simp]
    theorem Stream'.Discrete.principalOpen_append_nil {A : Type u_1} (a : Stream' A) (x : List A) :
    x ++ₛ a ∈ principalOpen x
    source
    @[simp]
    theorem Stream'.Discrete.principalOpen_cons_nil {A : Type u_1} (a : A) (as : Stream' A) :
    cons a as ∈ principalOpen [a]
    source
    @[simp]
    theorem Stream'.Discrete.extend_sub {A : Type u_1} (n : ℕ) (a : Stream' A) :
    a ∈ principalOpen (take n a)
    source
    theorem Stream'.Discrete.principalOpen_iff_restrict {A : Type u_1} (a : Stream' A) (x : List A) :
    a ∈ principalOpen x ↔ x = take x.length a
    source
    theorem Stream'.Discrete.principalOpen_cons {A : Type u_1} {as : Stream' A} {x : List A} {a : A} :
    as ∈ principalOpen (a :: x) ↔ as.get 0 = a ∧ as.tail ∈ principalOpen x
    source
    theorem Stream'.Discrete.principalOpen_index {A : Type u_1} (a : Stream' A) (x : List A) :
    a ∈ principalOpen x ↔ ∀ (n : ℕ) (x_1 : n < x.length), a.get n = x[n]
    source
    theorem Stream'.Discrete.principalOpen_concat {A : Type u_1} {as : Stream' A} {x : List A} {a : A} :
    as ∈ principalOpen (x ++ [a]) ↔ as ∈ principalOpen x ∧ as.get x.length = a
    source
    theorem Stream'.Discrete.principalOpen_restrict {A : Type u_1} (n : ℕ) (a b : Stream' A) :
    a ∈ principalOpen (take n b) ↔ ∀ m < n, a.get m = b.get m
    source
    @[simp]
    theorem Stream'.Discrete.principalOpen_sub {A : Type u_1} (x y : List A) :
    principalOpen (x ++ y) ⊆ principalOpen x
    source
    theorem Stream'.Discrete.principalOpen_mono {A : Type u_1} {x y : List A} (h : x <+: y) :
    principalOpen y ⊆ principalOpen x
    source
    theorem Stream'.Discrete.principalOpen_complement {A : Type u_1} (x : List A) :
    (principalOpen x)ᶜ = ⋃ (y : List A), ⋃ (_ : x.length = y.length ∧ x ≠ y), principalOpen y
    source
    @[instance_reducible]
    def Stream'.Discrete.prodDisc (A : Type u_3) :
    TopologicalSpace (Stream' A)

    Auxiliary declaration for the Borel determinacy formalization.

    Equations
    Instances For
      source
      @[instance_reducible]
      def Stream'.Discrete.instTopologicalSpaceLeanPool {A : Type u_1} :
      TopologicalSpace A

      Auxiliary declaration for the Borel determinacy formalization.

      Equations
      Instances For
        source
        theorem Stream'.Discrete.instDiscreteTopology_leanPool {A : Type u_1} :
        DiscreteTopology A
        source
        theorem Stream'.Discrete.continuous_pi' {A : Type u_1} {X : Type u_3} [TopologicalSpace X] {f : X → Stream' A} (h : ∀ (i : ℕ), Continuous fun (a : X) => (f a).get i) :
        Continuous f
        source
        theorem Stream'.Discrete.drop_con {A : Type u_1} (n : ℕ) :
        Continuous (drop n)
        source
        theorem Stream'.Discrete.tail_con {A : Type u_1} :
        Continuous tail
        source
        theorem Stream'.Discrete.append_con {A : Type u_1} (x : List A) :
        Continuous fun (x_1 : Stream' A) => x ++ₛ x_1
        source
        theorem Stream'.Discrete.hasBasis_principalOpen {A : Type u_1} (a : Stream' A) :
        (nhds a).HasBasis (fun (x : List A) => a ∈ principalOpen x) fun (x : List A) => principalOpen x

        The principal opens form a neighborhood basis for the product topology.

        source
        theorem Stream'.Discrete.hasBasis_principalOpen' {A : Type u_1} (m : ℕ) (a : Stream' A) :
        (nhds a).HasBasis (fun (n : ℕ) => n ≥ m) fun (n : ℕ) => principalOpen (take n a)
        source
        @[simp]
        theorem Stream'.Discrete.principalOpen_isOpen {A : Type u_1} (x : List A) :
        IsOpen (principalOpen x)
        source
        @[simp]
        theorem Stream'.Discrete.principalOpen_isClosed {A : Type u_1} (x : List A) :
        IsClosed (principalOpen x)