instance QuasiBorelSpace.Nat.instNat : QuasiBorelSpace ℕ

Equations

• QuasiBorelSpace.Nat.instNat = QuasiBorelSpace.ofMeasurableSpace

@[simp]

theorem QuasiBorelSpace.Nat.IsVar_def (φ : ℝ → ℕ) : IsVar φ = Measurable φ

theorem QuasiBorelSpace.Nat.isHom_rec {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {f : A → B} (hf : IsHom f) {g : A → ℕ → B → B} (hg : IsHom fun (x : A × ℕ × B) => match x with | (x, y, z) => g x y z) {h : A → ℕ} (hh : IsHom h) : IsHom fun (x : A) => Nat.rec (f x) (g x) (h x)

theorem QuasiBorelSpace.Nat.isHom_lt : IsHom fun (x : ℕ × ℕ) => x.1 < x.2

instance QuasiBorelSpace.Fin.instFin {n : ℕ} : QuasiBorelSpace (Fin n)

Equations

• QuasiBorelSpace.Fin.instFin = QuasiBorelSpace.ofMeasurableSpace

@[simp]

theorem QuasiBorelSpace.Fin.IsVar_def {n : ℕ} (φ : ℝ → Fin n) : IsVar φ = Measurable φ