theorem QuasiBorelSpace.Prop.isHom_ite {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {p : A → Prop} (hp : IsHom p) [inst : DecidablePred p] {f : A → B} (hf : IsHom f) {g : A → B} (hg : IsHom g) : IsHom fun (x : A) => if p x then f x else g x

theorem QuasiBorelSpace.Prop.isHom_not {A : Type u_1} [QuasiBorelSpace A] {f : A → Prop} (hf : IsHom f) : IsHom fun (x : A) => ¬f x

theorem QuasiBorelSpace.Prop.isHom_and {A : Type u_1} [QuasiBorelSpace A] {f g : A → Prop} (hf : IsHom f) (hg : IsHom g) : IsHom fun (x : A) => f x ∧ g x

theorem QuasiBorelSpace.Prop.isHom_or {A : Type u_1} [QuasiBorelSpace A] {f g : A → Prop} (hf : IsHom f) (hg : IsHom g) : IsHom fun (x : A) => f x ∨ g x

theorem QuasiBorelSpace.Prop.isHom_imp {A : Type u_1} [QuasiBorelSpace A] {f g : A → Prop} (hf : IsHom f) (hg : IsHom g) : IsHom fun (x : A) => f x → g x

theorem QuasiBorelSpace.Prop.isHom_iff {A : Type u_1} [QuasiBorelSpace A] {f g : A → Prop} (hf : IsHom f) (hg : IsHom g) : IsHom fun (x : A) => f x ↔ g x

theorem QuasiBorelSpace.Prop.isHom_forall {A : Type u_1} [QuasiBorelSpace A] {I : Sort u_3} [Countable I] {f : I → A → Prop} (hf : ∀ (i : I), IsHom (f i)) : IsHom fun (x : A) => ∀ (i : I), f i x

theorem QuasiBorelSpace.Prop.isHom_exists {A : Type u_1} [QuasiBorelSpace A] {I : Sort u_3} [Countable I] {f : I → A → Prop} (hf : ∀ (i : I), IsHom (f i)) : IsHom fun (x : A) => ∃ (i : I), f i x

theorem QuasiBorelSpace.Prop.isHom_dite {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {p : A → Prop} (hp : IsHom p) [inst : DecidablePred p] {f : (x : A) → p x → B} (hf : IsHom fun (x : Subtype p) => f ↑x ⋯) {g : (x : A) → ¬p x → B} (hg : IsHom fun (x : { x : A // ¬p x }) => g ↑x ⋯) : IsHom fun (x : A) => if h : p x then f x h else g x h

theorem QuasiBorelSpace.Prop.isHom_decide {A : Type u_1} [QuasiBorelSpace A] {p : A → Prop} [inst : DecidablePred p] (hp : IsHom p) : IsHom fun (x : A) => decide (p x)