LeanPool.QuasiBorelSpaces.Prop #
Imported Lean Pool material for LeanPool.QuasiBorelSpaces.Prop.
theorem
QuasiBorelSpace.Prop.isHom_ite
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
{p : A → Prop}
(hp : IsHom p)
[inst : DecidablePred p]
{f : A → B}
(hf : IsHom f)
{g : A → B}
(hg : IsHom g)
:
theorem
QuasiBorelSpace.Prop.isHom_not
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{f : A → Prop}
(hf : IsHom f)
:
theorem
QuasiBorelSpace.Prop.isHom_and
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{f g : A → Prop}
(hf : IsHom f)
(hg : IsHom g)
:
theorem
QuasiBorelSpace.Prop.isHom_or
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{f g : A → Prop}
(hf : IsHom f)
(hg : IsHom g)
:
theorem
QuasiBorelSpace.Prop.isHom_imp
{A : Type u_1}
{x✝ : 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}
{x✝ : QuasiBorelSpace A}
{f g : A → Prop}
(hf : IsHom f)
(hg : IsHom g)
:
theorem
QuasiBorelSpace.Prop.isHom_forall
{A : Type u_1}
{x✝ : 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}
{x✝ : 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}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : 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}
{x✝ : QuasiBorelSpace A}
{p : A → Prop}
[inst : DecidablePred p]
(hp : IsHom p)
: