diff --git a/Probability/Basic.lean b/Probability/Basic.lean index 6682b52..79343d4 100644 --- a/Probability/Basic.lean +++ b/Probability/Basic.lean @@ -1,3 +1,5 @@ +--Please add to main pretty pretty please +--Broke everything import Mathlib.Data.Nat.Basic import Mathlib.Data.Real.Basic import Mathlib.Data.Rat.Defs @@ -26,7 +28,7 @@ def indicator (cond : Bool) : β„š := cond.rec 0 1 abbrev 𝕀 : Bool β†’ β„š := indicator /-- Indicator is 0 or 1 -/ -theorem ind_zero_one (cond : Ο„ β†’ Bool) (Ο‰ : Ο„) : ( (π•€βˆ˜cond) Ο‰ = 1)∨((π•€βˆ˜cond) Ο‰ = 0) := by +theorem ind_zero_on (cond : Ο„ β†’ Bool) : ( (π•€βˆ˜cond) Ο‰ = 1)∨((π•€βˆ˜cond) Ο‰ = 0) := by by_cases h : cond Ο‰ Β· left; simp only [Function.comp_apply, h, indicator] Β· right; simp only [Function.comp_apply, h, indicator] diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index 19066fd..930fb30 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -9,6 +9,7 @@ % (no ugly rectangles around links). % It is otherwise a very minimal preamble (you should probably at least % add cleveref and tikz-cd). +% broke everything \documentclass[letterpaper]{article}