Theorem: PMF.mem_support_bernoulli'_iff (LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
⊢ b ∈ (bernoulli' p hp).support ↔ if b then p ≠ 0 else p ≠ 1
Tactic:
simp
State after:
no goals