forall_forall_merge' — Mathlib

English

A swap-variant of the Merge Lemma holds: the same equivalence with indices swapped.

Русский

Справедливость варианта с перестановкой индексов для леммы Merge: эквивалентность при перестановке индексов.

LaTeX

$$$ (\forall j,i:\mathbb{N},\ (c_0\,i)(c_1\,j)\le z) \iff \forall i:\mathbb{N},\ (c_0\,i)(c_1\,i)\le z$$$

Lean4

@[simp]
theorem forall_forall_merge' (c₀ : Chain (α →𝒄 β)) (c₁ : Chain α) (z : β) :
    (∀ j i : ℕ, (c₀ i) (c₁ j) ≤ z) ↔ ∀ i : ℕ, (c₀ i) (c₁ i) ≤ z := by rw [forall_swap, forall_forall_merge]

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