Theorems · Theorem · logic and foundations

Set.encard_eq_three

∀ {α : Type u_1} {s : Set α}, s.encard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Defined in

Mathlib.Data.Set.Card

Cited by

2 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound