monlib / preq.dite - mathlib3 docs

theorem dite_add_dite {α : Type u_1} [has_add α] (P : Prop) [decidable P] (a b : P → α) (c d : ¬P → α) :

dite P (λ (x : P), a x) (λ (x : ¬P), c x) + dite P (λ (x : P), b x) (λ (x : ¬P), d x) = dite P (λ (x : P), a x + b x) (λ (x : ¬P), c x + d x)

theorem smul_dite {α : Type u_1} (P : Prop) [decidable P] (a : P → α) (c : ¬P → α) {β : Type u_2} (r : β) [has_smul β α] :

r • dite P (λ (x : P), a x) (λ (x : ¬P), c x) = dite P (λ (x : P), r • a x) (λ (x : ¬P), r • c x)

theorem mul_dite {α : Type u_1} [has_mul α] (P : Prop) [decidable P] (a : α) (b : P → α) (c : ¬P → α) :

a * dite P (λ (x : P), b x) (λ (x : ¬P), c x) = dite P (λ (x : P), a * b x) (λ (x : ¬P), a * c x)

theorem dite_mul {α : Type u_1} [has_mul α] (P : Prop) [decidable P] (a : α) (b : P → α) (c : ¬P → α) :

dite P (λ (x : P), b x) (λ (x : ¬P), c x) * a = dite P (λ (x : P), b x * a) (λ (x : ¬P), c x * a)

theorem dite_boole_add {α : Type u_1} [add_zero_class α] (P : Prop) [decidable P] (a b : P → α) :

dite P (λ (x : P), a x + b x) (λ (x : ¬P), 0) = dite P (λ (x : P), a x) (λ (x : ¬P), 0) + dite P (λ (x : P), b x) (λ (x : ¬P), 0)

theorem dite_boole_smul {α : Type u_1} {β : Type u_2} [has_zero α] [smul_zero_class β α] (P : Prop) [decidable P] (a : P → α) (r : β) :

dite P (λ (x : P), r • a x) (λ (x : ¬P), 0) = r • dite P (λ (x : P), a x) (λ (x : ¬P), 0)

theorem star_dite (P : Prop) [decidable P] {α : Type u_1} [has_involutive_star α] (a : P → α) (b : ¬P → α) :

has_star.star (dite P (λ (i : P), a i) (λ (i : ¬P), b i)) = dite P (λ (i : P), has_star.star (a i)) (λ (i : ¬P), has_star.star (b i))

theorem dite_tmul {R : Type u_1} {N₁ : Type u_2} {N₂ : Type u_3} [comm_semiring R] [add_comm_group N₁] [add_comm_group N₂] [module R N₁] [module R N₂] (P : Prop) [decidable P] (x₁ : P → N₁) (x₂ : N₂) :

dite P (λ (h : P), x₁ h) (λ (h : ¬P), 0) ⊗ₜ[R] x₂ = dite P (λ (h : P), x₁ h ⊗ₜ[R] x₂) (λ (h : ¬P), 0)

theorem tmul_dite {R : Type u_1} {N₁ : Type u_2} {N₂ : Type u_3} [comm_semiring R] [add_comm_group N₁] [add_comm_group N₂] [module R N₁] [module R N₂] (P : Prop) [decidable P] (x₁ : N₁) (x₂ : P → N₂) :

x₁ ⊗ₜ[R] dite P (λ (h : P), x₂ h) (λ (h : ¬P), 0) = dite P (λ (h : P), x₁ ⊗ₜ[R] x₂ h) (λ (h : ¬P), 0)

theorem linear_map.apply_dite {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [semiring R] [add_comm_monoid H₁] [add_comm_monoid H₂] [module R H₁] [module R H₂] (f : H₁ →ₗ[R] H₂) (P : Prop) [decidable P] (a : P → H₁) (b : ¬P → H₁) :

⇑f (dite P (λ (h : P), a h) (λ (h : ¬P), b h)) = dite P (λ (h : P), ⇑f (a h)) (λ (h : ¬P), ⇑f (b h))

mathlib3 documentation