eq_empty_of_sym_eq_empty

Mathlib.Data.Finset.Sym

URI: https://scilib.ai/kg/mathlib#Finset.eq_empty_of_sym_eq_empty

English

If s.sym n = ∅, then s = ∅.

Русский

Если s.sym n = ∅, то s = ∅.

LaTeX

$$s.sym n = ∅ \Rightarrow s = ∅$$

Lean4

theorem eq_empty_of_sym_eq_empty (h : s.sym n = ∅) : s = ∅ :=
  by
  rw [← not_nonempty_iff_eq_empty] at h ⊢
  exact fun hs ↦ h (hs.sym _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru