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⟩⟩