cons_le_cons — Mathlib

English

Let x0,y0 ∈ α0 and x,y ∈ ∀ i ∈ Fin n, α(i.succ). Then cons x0 x ≤ cons y0 y iff x0 ≤ y0 and x ≤ y.

Русский

Пусть x0,y0 ∈ α0 и x,y ∈ ∀ i ∈ Fin n, α(i.succ). Тогда cons x0 x ≤ cons y0 y тогда и только если x0 ≤ y0 и x ≤ y.

LaTeX

$$$\\text{cons } x_0 x \\le \\text{cons } y_0 y \\iff x_0 \\le y_0 \\land x \\le y.$$$

Lean4

theorem cons_le_cons [∀ i, Preorder (α i)] {x₀ y₀ : α 0} {x y : ∀ i : Fin n, α i.succ} :
    cons x₀ x ≤ cons y₀ y ↔ x₀ ≤ y₀ ∧ x ≤ y :=
  forall_fin_succ.trans <| and_congr_right' <| by simp only [cons_succ, Pi.le_def]

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