English
If there exist a in α with Nonempty (β a) and b with IsEmpty (β b), then WType β is Infinite.
Русский
Если существует a в α с ненулевым β a и существет b, для которого β b пусто, то WType β бесконечен.
LaTeX
$$$(\exists a:\alpha, Nonempty(β(a))) \land (\exists b:\alpha, IsEmpty(β(b))) \Rightarrow \text{Infinite}(WType(β)).$$$
Lean4
theorem infinite_of_nonempty_of_isEmpty (a b : α) [ha : Nonempty (β a)] [he : IsEmpty (β b)] : Infinite (WType β) :=
⟨by
intro hf
have hba : b ≠ a := fun h => ha.elim (IsEmpty.elim' (show IsEmpty (β a) from h ▸ he))
refine
not_injective_infinite_finite
(fun n : ℕ => show WType β from Nat.recOn n ⟨b, IsEmpty.elim' he⟩ fun _ ih => ⟨a, fun _ => ih⟩) ?_
intro n m h
induction n generalizing m with
| zero => rcases m with - | m <;> simp_all
| succ n ih =>
rcases m with - | m
· simp_all
· refine congr_arg Nat.succ (ih ?_)
simp_all [funext_iff]⟩
