LeanPool.QuasiBorelSpaces.Lift

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.Lift.

@[instance_reducible]

instance QuasiBorelSpace.ULift.instULift {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (ULift.{u_3, u_1} A)

Equations

• QuasiBorelSpace.ULift.instULift = QuasiBorelSpace.lift ULift.down

@[simp]

theorem QuasiBorelSpace.ULift.isHom_def {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {φ : A → ULift.{u_3, u_2} B} : IsHom φ ↔ IsHom fun (x : A) => (φ x).down

theorem QuasiBorelSpace.ULift.isHom_up {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} (hf : IsHom f) : IsHom fun (x : A) => { down := f x }

theorem QuasiBorelSpace.ULift.isHom_down {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → ULift.{u_3, u_2} B} (hf : IsHom f) : IsHom fun (x : A) => (f x).down

@[instance_reducible]

instance QuasiBorelSpace.PLift.instPLift {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (PLift A)

Equations

• QuasiBorelSpace.PLift.instPLift = QuasiBorelSpace.lift PLift.down

@[simp]

theorem QuasiBorelSpace.PLift.isHom_def {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {φ : A → PLift B} : IsHom φ ↔ IsHom fun (x : A) => (φ x).down

theorem QuasiBorelSpace.PLift.isHom_up {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} (hf : IsHom f) : IsHom fun (x : A) => { down := f x }

theorem QuasiBorelSpace.PLift.isHom_down {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → PLift B} (hf : IsHom f) : IsHom fun (x : A) => (f x).down