rel_flatten — Mathlib

English

Flattening nested lists interacts with Forall₂: Forall₂ (Forall₂ R) on nested lists implies Forall₂ R on the flattened lists.

Русский

Слияние вложенных списков в Forall₂ взаимодействует так, что Forall₂ (Forall₂ R) над вложенными списками приводит к Forall₂ R над уплощёнными списками.

LaTeX

$$$ \mathrm{rel\_flatten} : (\mathrm{Forall₂}\ (\mathrm{Forall₂}\ R) \Rightarrow \mathrm{Forall₂}\ R) \ \mathrm{flatten}\ \mathrm{flatten}$$$

Lean4

theorem rel_flatten : (Forall₂ (Forall₂ R) ⇒ Forall₂ R) flatten flatten
  | [], [], Forall₂.nil => Forall₂.nil
  | _, _, Forall₂.cons h₁ h₂ => rel_append h₁ (rel_flatten h₂)

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