snd

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#WCovBy.snd

← MathLib Explorer

English

If h: x ⩿ y, then the second projection preserves the weak cover: x.2 ⩿ y.2.

Русский

Если h: x ⩿ y, то вторая проекция сохраняет слабое покрытие: x.2 ⩿ y.2.

LaTeX

$$$ h : x \covby y \Rightarrow x.2 \covby y.2 $$$

Lean4

theorem _root_.WCovBy.snd (h : x ⩿ y) : x.2 ⩿ y.2 :=
  ⟨h.1.2, fun _ h₁ h₂ => h.2 (mk_lt_mk_iff_right.2 h₁) ⟨⟨h.1.1, h₂.le⟩, fun hc => h₂.not_ge hc.2⟩⟩

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

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

Разделы

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

Аффилиация

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