forall₂_cons_right_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem forall₂_cons_right_iff {b l u} : Forall₂ R u (b :: l) ↔ ∃ a u', R a b ∧ Forall₂ R u' l ∧ u = a :: 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₂

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