reachable_boxProd — Mathlib

English

In the box (Cartesian) product, a pair x=(a,b) is reachable from y=(a',b') if and only if a is reachable to a' in G and b is reachable to b' in H.

Русский

В декартовом произведении пара (a,b) достижима из (a',b') тогда и только тогда a достижимо до a' в G и b достижимо до b' в H.

LaTeX

$$$ (G \square H).Reachable x y \iff G.Reachable x.1 y.1 \land H.Reachable x.2 y.2, \quad x=(x.1,x.2), y=(y.1,y.2).$$$

Lean4

theorem reachable_boxProd {x y : α × β} : (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2 := by
  classical
  constructor
  · intro ⟨w⟩
    exact ⟨⟨w.ofBoxProdLeft⟩, ⟨w.ofBoxProdRight⟩⟩
  · intro ⟨⟨w₁⟩, ⟨w₂⟩⟩
    exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩

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