quasi-borel-spaces/QuasiBorelSpaces/Lift.lean at main · YellPika/quasi-borel-spaces · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
import QuasiBorelSpaces.Basic

variable {A B : Type*} [QuasiBorelSpace A] [QuasiBorelSpace B]

namespace QuasiBorelSpace.ULift

instance : QuasiBorelSpace (ULift A) := lift ULift.down

@[simp]
lemma isHom_def {φ : A → ULift B} : IsHom φ ↔ IsHom (fun x ↦ (φ x).down) := by
  simp only [isHom_to_lift]

@[fun_prop]
lemma isHom_up {f : A → B} (hf : IsHom f) : IsHom (fun x ↦ ULift.up (f x)) := by
  simp only [isHom_def, hf]

@[fun_prop]
lemma isHom_down {f : A → ULift B} (hf : IsHom f) : IsHom (fun x ↦ ULift.down (f x)) := by
  simp only [isHom_def] at hf
  exact hf

end QuasiBorelSpace.ULift

namespace QuasiBorelSpace.PLift

instance : QuasiBorelSpace (PLift A) := lift PLift.down

@[simp]
lemma isHom_def {φ : A → PLift B} : IsHom φ ↔ IsHom (fun x ↦ (φ x).down) := by
  simp only [isHom_to_lift]

@[fun_prop]
lemma isHom_up {f : A → B} (hf : IsHom f) : IsHom (fun x ↦ PLift.up (f x)) := by
  simp only [isHom_def, hf]

@[fun_prop]
lemma isHom_down {f : A → PLift B} (hf : IsHom f) : IsHom (fun x ↦ PLift.down (f x)) := by
  simp only [isHom_def] at hf
  exact hf

end QuasiBorelSpace.PLift