antisymm

Mathlib.Data.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.Subset.antisymm

English

If s1 ⊆ s2 and s2 ⊆ s1, then s1 = s2.

Русский

Если s1 ⊆ s2 и s2 ⊆ s1, то s1 = s2.

LaTeX

$$$s_1 \subseteq s_2 \to s_2 \subseteq s_1 \to s_1 = s_2$$$

Lean4

theorem antisymm {s₁ s₂ : Finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
  ext fun a => ⟨@H₁ a, @H₂ a⟩

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

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

Разделы

Аффилиация

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