LeanPool.QuasiBorelSpaces.Nat

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.Nat.

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

theorem QuasiBorelSpace.Nat.isHom_lt' {A : Type u_1} [QuasiBorelSpace A] {f : A → ℕ} (hf : IsHom f) {g : A → ℕ} (hg : IsHom g) : IsHom fun (x : A) => f x < g x

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

theorem QuasiBorelSpace.Nat.isHom_add' {A : Type u_1} [QuasiBorelSpace A] {f : A → ℕ} (hf : IsHom f) {g : A → ℕ} (hg : IsHom g) : IsHom fun (x : A) => f x + g x

theorem QuasiBorelSpace.Nat.isHom_find {A : Type u_1} [QuasiBorelSpace A] {p : A → ℕ → Prop} [(x : A) → DecidablePred (p x)] {q : ∀ (x : A), ∃ (n : ℕ), p x n} (hp : ∀ (n : ℕ), IsHom fun (x : A) => p x n) : IsHom fun (x : A) => Nat.find ⋯

@[instance_reducible]

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 φ