pith. machine review for the scientific record. sign in
theorem proved term proof

separable_implies_zero_mixed_diff

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 105theorem separable_implies_zero_mixed_diff (P : ℝ → ℝ → ℝ) (hSep : IsSeparable P) :
 106    ∀ u₀ v₀ u₁ v₁, P u₁ v₁ - P u₁ v₀ - P u₀ v₁ + P u₀ v₀ = 0 := by

proof body

Term-mode proof.

 107  obtain ⟨α, β, h⟩ := hSep
 108  intro u₀ v₀ u₁ v₁
 109  simp only [h]
 110  ring
 111
 112/-- Separable implies not entangling (contrapositive of entangling implies not separable). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.