forall₂_cons_left_iff — Mathlib

English

For all a, l, u, Forall₂ R (a :: l) u is equivalent to there exist b, u' with R a b and Forall₂ R l u' and u = b :: u'.

Русский

Для всех a,l,u: Forall₂ R (a :: l) u эквивалентно существованию b, u' such что R a b, Forall₂ R l u' и u = b :: u'.

LaTeX

$$$$ (\\forall a\\, l\\, u,\\ Forall₂\\ R\\ (a::l)\\ u) \\iff \\exists b\\;\\exists u',\\ R\\ a\\ b \\land Forall₂\\ R\\ l\\ u' \\land u = b::u'. $$$$

Lean4

theorem forall₂_cons_left_iff {a l u} : Forall₂ R (a :: l) u ↔ ∃ b u', R a b ∧ Forall₂ R l u' ∧ u = b :: u' :=
  Iff.intro
    (fun h =>
      match u, h with
      | b :: u', Forall₂.cons h₁ h₂ => ⟨b, u', h₁, h₂, rfl⟩)
    fun h =>
    match u, h with
    | _, ⟨_, _, h₁, h₂, rfl⟩ => Forall₂.cons h₁ h₂

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