Binary Coproducts of Quasi-Borel Spaces

This file defines binary coproducts of quasi-borel spaces by giving a QuasiBorelSpace instance for the Sum (⊕) type.

See [HKSY17], Proposition 17.

def QuasiBorelSpace.Sum.Encoding (A : Type u) (B : Type v) : Bool → Type (max u v)

We derive the QuasiBorelSpace instance for A ⊕ B via Sigma (Encoding A B).

Equations

• QuasiBorelSpace.Sum.Encoding A B true = ULift.{?u.1, ?u.2} A
• QuasiBorelSpace.Sum.Encoding A B false = ULift.{?u.4, ?u.3} B

def QuasiBorelSpace.Sum.Encoding.inl {A : Type u_1} {B : Type u_2} (x : A) : Sigma (Sum.Encoding A B)

The encoded version of Sum.inl.

Equations

• QuasiBorelSpace.Sum.Encoding.inl x = ⟨true, { down := x }⟩

def QuasiBorelSpace.Sum.Encoding.inr {A : Type u_1} {B : Type u_2} (x : B) : Sigma (Sum.Encoding A B)

The encoded version of Sum.inr.

Equations

• QuasiBorelSpace.Sum.Encoding.inr x = ⟨false, { down := x }⟩

def QuasiBorelSpace.Sum.Encoding.elim {A : Type u_1} {B : Type u_2} {C : Type u_3} (f : A → C) (g : B → C) : Sigma (Sum.Encoding A B) → C

The encoded version of Sum.elim.

Equations

• QuasiBorelSpace.Sum.Encoding.elim f g ⟨true, x_1⟩ = f x_1.down
• QuasiBorelSpace.Sum.Encoding.elim f g ⟨false, x_1⟩ = g x_1.down

@[instance_reducible]

instance QuasiBorelSpace.Sum.Encoding.inst {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {b : Bool} : QuasiBorelSpace (Sum.Encoding A B b)

Equations

• One or more equations did not get rendered due to their size.

def QuasiBorelSpace.Sum.encode {A : Type u_1} {B : Type u_2} : A ⊕ B → Sigma (Sum.Encoding A B)

Encodes an A ⊕ B as a Sigma (Encoding A B).

Equations

• QuasiBorelSpace.Sum.encode = Sum.elim QuasiBorelSpace.Sum.Encoding.inl QuasiBorelSpace.Sum.Encoding.inr

@[instance_reducible]

instance QuasiBorelSpace.Sum.instSum {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] : QuasiBorelSpace (A ⊕ B)

Equations

• QuasiBorelSpace.Sum.instSum = QuasiBorelSpace.lift QuasiBorelSpace.Sum.encode