inter

Mathlib.SetTheory.ZFC.Ordinal

URI: https://scilib.ai/kg/mathlib#ZFSet.IsTransitive.inter

← MathLib Explorer

English

The intersection of two transitive sets is transitive.

Русский

Пересечение двух транзитивных множеств транзитивно.

LaTeX

$$$ (x.IsTransitive) \\to (y.IsTransitive) \\to (x \\cap y).IsTransitive. $$$

Lean4

protected theorem inter (hx : x.IsTransitive) (hy : y.IsTransitive) : (x ∩ y).IsTransitive := fun z hz w hw =>
  by
  rw [mem_inter] at hz ⊢
  exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩

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

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

Разделы

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

Аффилиация

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