superset_antisymm_iff

Mathlib.Order.RelClasses

URI: https://scilib.ai/kg/mathlib#superset_antisymm_iff

← MathLib Explorer

English

a = b if and only if b ⊆ a and a ⊆ b.

Русский

a = b тогда и только тогда, когда b ⊆ a и a ⊆ b.

LaTeX

$$$a = b \iff (b \subseteq a \land a \subseteq b)$$$

Lean4

theorem superset_antisymm_iff [IsRefl α (· ⊆ ·)] [IsAntisymm α (· ⊆ ·)] : a = b ↔ b ⊆ a ∧ a ⊆ b :=
  ⟨fun h => ⟨h.superset, h.subset'⟩, fun h => h.1.antisymm' h.2⟩

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

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

Разделы

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

Аффилиация

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