`BookProof.ChapterEulerStochastic.preservesProb_iff_columnStochastic` (M : Matrix (Fin 2) (Fin 2) ℝ) : PreservesProb M ↔ (IsProbVec (fun i => M i 0) ∧ IsProbVec (fun i => M i 1))

Proved

BookProof.ChapterEulerStochastic.preservesProb_iff_columnStochastic

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterEulerStochastic.

BookProof.ChapterEulerStochastic.preservesProb_iff_columnStochastic (M : Matrix (Fin 2) (Fin 2) ℝ) : PreservesProb M ↔ (IsProbVec (fun i => M i 0) ∧ IsProbVec (fun i => M i 1))

Formalization note: Lean 4 identifier BookProof.ChapterEulerStochastic.preservesProb_iff_columnStochastic.

Preamble

-- Generated from ChapterEulerStochastic.lean — theorem BookProof.ChapterEulerStochastic.preservesProb_iff_columnStochastic
import Mathlib
import Definitions.Def_ChapterEulerStochastic
open BookProof.ChapterEulerStochastic


open scoped Matrix BigOperators

Formal statement

theorem BookProof.ChapterEulerStochastic.preservesProb_iff_columnStochastic (M : Matrix (Fin 2) (Fin 2) ℝ) :
    PreservesProb M ↔
      (IsProbVec (fun i => M i 0) ∧ IsProbVec (fun i => M i 1)) := by sorry

View graph