trans — Mathlib

English

If p ≤₀ q and q ≤₀ r then p ≤₀ r.

Русский

Если p редуцируется к q, а q к r, то p редуцируется к r.

LaTeX

$$$\forall {\alpha \beta \gamma} [Primcodable \alpha][Primcodable \beta][Primcodable \gamma],\forall p:\alpha\to Prop, q:\beta\to Prop, r:\gamma\to Prop,\ p \le_0 q \to q \le_0 r \to p \le_0 r$$$

Lean4

@[trans]
theorem trans {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :
    p ≤₀ q → q ≤₀ r → p ≤₀ r
  | ⟨f, c₁, h₁⟩, ⟨g, c₂, h₂⟩ =>
    ⟨g ∘ f, c₂.comp c₁, fun a => ⟨fun h => by rw [comp_apply, ← h₂, ← h₁]; assumption, fun h => by rwa [h₁, h₂]⟩⟩

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