antisymm_iff

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.Subset.antisymm_iff

← MathLib Explorer

English

For sets a,b, a = b iff a ⊆ b and b ⊆ a.

Русский

Для множеств a,b верно: a = b тогда и только тогда, когда a ⊆ b и b ⊆ a.

LaTeX

$$$\\forall {a,b\\subseteq\\alpha},\\ a=b \\iff (a\\subset b \\land b\\subset a)$$$

Lean4

theorem antisymm_iff {a b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a :=
  ⟨fun e => ⟨e.subset, e.symm.subset⟩, fun ⟨h₁, h₂⟩ => Subset.antisymm h₁ h₂⟩
    -- an alternative name

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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