chainHeight_mono

Mathlib.Order.Height

URI: https://scilib.ai/kg/mathlib#Set.chainHeight_mono

← MathLib Explorer

English

If s ⊆ t, then s.chainHeight ≤ t.chainHeight.

Русский

Если s ⊆ t, то s.chainHeight ≤ t.chainHeight.

LaTeX

$$(s ⊆ t) ⇒ s.chainHeight ≤ t.chainHeight$$

Lean4

theorem chainHeight_mono (h : s ⊆ t) : s.chainHeight ≤ t.chainHeight :=
  chainHeight_le_chainHeight_iff.2 fun l hl ↦ ⟨l, ⟨hl.1, fun i hi ↦ h <| hl.2 i hi⟩, rfl⟩

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

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

Разделы

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

Аффилиация

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