@[reducible, inline]

abbrev QuasiBorelSpace.Option.Encoding (A : Type u_4) : Type u_4

We derive the QuasiBorelSpace instance for Option As from their encoding as Unit ⊕ A.

Equations

• QuasiBorelSpace.Option.Encoding A = (Unit ⊕ A)

def QuasiBorelSpace.Option.Encoding.none {A : Type u_1} : Encoding A

The encoded version of Option.none.

Equations

• QuasiBorelSpace.Option.Encoding.none = Sum.inl ()

def QuasiBorelSpace.Option.Encoding.some {A : Type u_1} (x : A) : Encoding A

The encoded version of Option.some.

Equations

• QuasiBorelSpace.Option.Encoding.some x = Sum.inr x

def QuasiBorelSpace.Option.Encoding.elim {A : Type u_1} {B : Type u_2} (x : B) (f : A → B) : Encoding A → B

The encoded version of Option.elim.

Equations

• QuasiBorelSpace.Option.Encoding.elim x f = Sum.elim (fun (x_1 : Unit) => x) f

@[simp]

theorem QuasiBorelSpace.Option.Encoding.isHom_some {A : Type u_1} [QuasiBorelSpace A] : IsHom some

theorem QuasiBorelSpace.Option.Encoding.isHom_elim {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : A → C} (hf : IsHom f) {g : A → B → C} (hg : IsHom fun (x : A × B) => match x with | (x, y) => g x y) {h : A → Encoding B} (hh : IsHom h) : IsHom fun (x : A) => elim (f x) (g x) (h x)

def QuasiBorelSpace.Option.encode {A : Type u_1} (x : Option A) : Unit ⊕ A

Encodes an Option A as an Encoding A.

Equations

• QuasiBorelSpace.Option.encode x = x.elim QuasiBorelSpace.Option.Encoding.none QuasiBorelSpace.Option.Encoding.some

instance QuasiBorelSpace.Option.instOption {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (Option A)

Equations

• QuasiBorelSpace.Option.instOption = QuasiBorelSpace.lift QuasiBorelSpace.Option.encode

@[simp]

theorem QuasiBorelSpace.Option.isHom_encode {A : Type u_1} [QuasiBorelSpace A] : IsHom encode

theorem QuasiBorelSpace.Option.isHom_some {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} (hf : IsHom f) : IsHom fun (x : A) => some (f x)

theorem QuasiBorelSpace.Option.isHom_elim {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : A → Option B} (hf : IsHom f) {g : A → C} (hg : IsHom g) {h : A → B → C} (hh : IsHom fun (x : A × B) => match x with | (x, y) => h x y) : IsHom fun (x : A) => (f x).elim (g x) (h x)

theorem QuasiBorelSpace.Option.isHom_map {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : A → B → C} (hf : IsHom fun (x : A × B) => match x with | (x, y) => f x y) {g : A → Option B} (hg : IsHom g) : IsHom fun (x : A) => Option.map (f x) (g x)

theorem QuasiBorelSpace.Option.isHom_getD {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → Option B} (hf : IsHom f) {g : A → B} (hg : IsHom g) : IsHom fun (x : A) => (f x).getD (g x)

instance QuasiBorelSpace.Option.instIsHomDiagonalOption {A : Type u_1} [QuasiBorelSpace A] [IsHomDiagonal A] : IsHomDiagonal (Option A)