English
The support of bernoulli(p,h) is the set {b ∈ Bool : cond b (p ≠ 0) (p ≠ 1)}.
Русский
Поддержка Bernoulli(p,h) есть множество {b ∈ Bool : cond(b, p ≠ 0, p ≠ 1)}.
LaTeX
$$$ (\mathrm{bernoulli}(p,h)).\mathrm{support} = \{ b \in \mathrm{Bool} \mid \operatorname{cond}(b, p \neq 0, p \neq 1) \} $$$
Lean4
@[simp]
theorem support_bernoulli : (bernoulli p h).support = {b | cond b (p ≠ 0) (p ≠ 1)} :=
by
refine Set.ext fun b => ?_
induction b
· simp_rw [mem_support_iff, bernoulli_apply, Bool.cond_false, Ne, ENNReal.coe_sub, ENNReal.coe_one, Bool.cond_prop,
Set.mem_setOf_eq, Bool.false_eq_true, ite_false, not_iff_not]
constructor
· intro h'
simp only [tsub_eq_zero_iff_le, one_le_coe_iff] at h'
exact eq_of_le_of_ge h h'
· intro h'
simp only [h', ENNReal.coe_one, tsub_self]
· simp only [mem_support_iff, bernoulli_apply, Bool.cond_true, Set.mem_setOf_eq, ne_eq, ENNReal.coe_eq_zero]