univ_finset_eq_singleton_empty_iff

English

For any α, the univ Finset equals {∅} if and only if α is empty.

Русский

Для любого α универcальный финсет равен {∅} тогда и только тогда, когда α пуст.

LaTeX

$$$ \\\\forall {\\alpha} : \\\\mathrm{Type}, [IsEmpty \\\\alpha] \\\\Rightarrow \\\\mathrm{Set.univ} (Finset \\\\alpha) = \\\\{\\\\emptyset\\\\}$$$

Lean4

@[simp]
theorem univ_finset_eq_singleton_empty_iff : @Set.univ (Finset α) = {∅} ↔ IsEmpty α :=
  ⟨fun h ↦ isEmpty_of_forall_eq_empty fun s ↦ Set.mem_singleton_iff.mp (Set.ext_iff.mp h s |>.mp (Set.mem_univ s)),
    fun _ ↦ by simp⟩

Похожие утверждения