fst

Mathlib.Order.Cover

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

← MathLib Explorer

English

If h: x ⩿ y, then the first projection preserves the weak cover: x.1 ⩿ y.1.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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