Prove2Me

Equivalence_Class_is_not_Empty

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

empty-setequivalence-classesfundamental-theorem-on-equivalence-relationsproofwiki

Let R be an equivalence relation on a set S. Then no equivalence class is empty.

Preamble
import Mathlib.Data.Setoid.Basic
import Mathlib.Data.Set.Basic
Formal statement
theorem Equivalence_Class_is_not_Empty {α : Type _} (s : Setoid α) (x : α) : Set.Nonempty {y | s.r x y} := by sorry
Source
https://proofwiki.org/wiki/Equivalence_Class_is_not_Empty

View graph