α : Type u_1
β : Type ?u.55273
s t : Finset α
f : α → β
n : ℕ
⊢ ¬1 < card s ↔ ¬∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b
α : Type u_1
β : Type ?u.55273
s t : Finset α
f : α → β
n : ℕ
⊢ 1 < card s ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b
rw [← not_iff_not]
α : Type u_1
β : Type ?u.55273
s t : Finset α
f : α → β
n : ℕ
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
α : Type u_1
β : Type ?u.55273
s t : Finset α
f : α → β
n : ℕ
⊢ ¬1 < card s ↔ ¬∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b
push_neg
no goals
α : Type u_1
β : Type ?u.55273
s t : Finset α
f : α → β
n : ℕ
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
exact card_le_one