Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari
Created December 12, 2019 11:38
Show Gist options
  • Save mukeshtiwari/f5692ca8bacac1c2bcb44386194a0e2a to your computer and use it in GitHub Desktop.
Save mukeshtiwari/f5692ca8bacac1c2bcb44386194a0e2a to your computer and use it in GitHub Desktop.
section disprob
parameters (Ω : Type) [fintype Ω]
parameters (uniform : Ω → ℚ)
parameters (Huniform : ∀ x : Ω, uniform x = 1 / (fintype.card Ω))
lemma prob_sum : match (fintype.exists_univ_list Ω) with
| (l, _) := list.sum (list.map l) = 1
end :=
begin
sorry
end
end disprob
invalid match/convoy expression, expected type is not knownLean
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment