instHasSSubset

Mathlib.SetTheory.ZFC.PSet

URI: https://scilib.ai/kg/mathlib#PSet.instHasSSubset

English

For any x,y, x ≃ y iff x ⊆ y and y ⊆ x.

Русский

Для любых x, y: x ≃ y тогда и только тогда, когда x ⊆ y и y ⊆ x.

LaTeX

$$$\\\\forall x,y:\\\\mathrm{PSet},\\\\ x\\\\simeq y \\\\Longleftrightarrow \\\\ (x\\\\subseteq y) \\\\land (y\\\\subseteq x)$$$

Lean4

instance : HasSSubset PSet :=
  ⟨(· < ·)⟩

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

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

Разделы

Аффилиация

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