forall_rel_cons_ext — Mathlib

English

A pointwise extension of relation r through cons preserves the relation if the base hypotheses hold for all elements in the tail.

Русский

Расширение по точкам через cons сохраняет отношение r при выполнении исходных условий для всех элементов хвоста.

LaTeX

$$$\\forall a\\ ha, r (\\mathrm{cons} \\ _ b_1 \\ f_1 a ha) (\\mathrm{cons} \\ _ b_2 \\ f_2 a ha).$$$

Lean4

theorem forall_rel_cons_ext {r : ∀ ⦃a⦄, δ a → δ a → Prop} {b₁ b₂ : δ a} {f₁ f₂ : ∀ a' ∈ m, δ a'} (hb : r b₁ b₂)
    (hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)) : ∀ a ha, r (cons _ _ b₁ f₁ a ha) (cons _ _ b₂ f₂ a ha) :=
  by
  intro a ha
  dsimp [cons]
  split_ifs with H
  · cases H
    exact hb
  · exact hf _ _

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