toFinset_inj — Mathlib

English

The map s ↦ s.toFinset is injective on Set under Finite types: if s.toFinset = t.toFinset then s = t.

Русский

Отображение s ↦ s.toFinset инъективно на множествах при конечных множествах: если s.toFinset = t.toFinset, то s = t.

LaTeX

$$$s.toFinset = t.toFinset \iff s = t$$$

Lean4

@[simp]
theorem toFinset_inj {s t : Set α} [Fintype s] [Fintype t] : s.toFinset = t.toFinset ↔ s = t :=
  ⟨fun h => by rw [← s.coe_toFinset, h, t.coe_toFinset], fun h => by simp [h]⟩

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