trans_left — Mathlib

English

If Wbtw R w y z and Wbtw R w x y hold, then Wbtw R w x z holds.

Русский

Если Wbtw R w y z и Wbtw R w x y выполняются, тогда Wbtw R w x z выполняется.

LaTeX

$$$$ Wbtw R w y z \to Wbtw R w x y \to Wbtw R w x z $$$$

Lean4

theorem trans_left {w x y z : P} (h₁ : Wbtw R w y z) (h₂ : Wbtw R w x y) : Wbtw R w x z :=
  by
  rcases h₁ with ⟨t₁, ht₁, rfl⟩
  rcases h₂ with ⟨t₂, ht₂, rfl⟩
  refine ⟨t₂ * t₁, ⟨mul_nonneg ht₂.1 ht₁.1, mul_le_one₀ ht₂.2 ht₁.1 ht₁.2⟩, ?_⟩
  rw [lineMap_apply, lineMap_apply, lineMap_vsub_left, smul_smul]

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