isTransitive_iff_subset_powerset

Mathlib.SetTheory.ZFC.Ordinal

URI: https://scilib.ai/kg/mathlib#ZFSet.isTransitive_iff_subset_powerset

← MathLib Explorer

English

A set x is transitive iff x ⊆ powerset x.

Русский

Множество x транзитивно тогда и только тогда, когда x ⊆ powerset x.

LaTeX

$$$ x.IsTransitive \\iff x \\subseteq \\mathrm{powerset}\\, x. $$$

Lean4

theorem isTransitive_iff_subset_powerset : x.IsTransitive ↔ x ⊆ powerset x :=
  ⟨fun h _ hy => mem_powerset.2 <| h.subset_of_mem hy, fun H _ hy _ hz => mem_powerset.1 (H hy) hz⟩

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

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

Разделы

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

Аффилиация

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