subset_iff

Mathlib.SetTheory.ZFC.PSet

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

English

x ⊆ y iff every z ∈ x is also in y.

Русский

x ⊆ y тогда и только тогда, когда каждый z ∈ x принадлежит y.

LaTeX

$$$\\forall {x y : PSet},\\ x\\subseteq y \\iff \\forall {z}, z\\in x \\rightarrow z\\in y$$$

Lean4

theorem subset_iff {x y : PSet} : x ⊆ y ↔ ∀ ⦃z⦄, z ∈ x → z ∈ y :=
  ⟨fun h _ => mem_of_subset h, fun h a => h (Mem.mk _ a)⟩

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

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

Разделы

Аффилиация

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