English
Let c0 be a chain of monotone maps α →𝒄 β and c1 a chain α with bound z ∈ β. Then the bound condition holding for all indices is equivalent to it holding along the diagonal (i,i).
Русский
Пусть c0 — цепь монотонных отображений α →𝒄 β, a цепь c1 из α и элемент z ∈ β. Утверждение о нижней/верхней границе через все индексы эквивалентно утверждению на диагонали (i,i).
LaTeX
$$$ (\forall i,j:\mathbb{N},\ (c_0\,i)(c_1\,j)\le z) \iff \forall i:\mathbb{N},\ (c_0\,i)(c_1\,i)\le z$$$
Lean4
/-- When proving that a chain of applications is below a bound `z`, it suffices to consider the
functions and values being selected from the same index in the chains.
This lemma is more specific than necessary, i.e. `c₀` only needs to be a
chain of monotone functions, but it is only used with continuous functions. -/
@[simp]
theorem forall_forall_merge (c₀ : Chain (α →𝒄 β)) (c₁ : Chain α) (z : β) :
(∀ i j : ℕ, (c₀ i) (c₁ j) ≤ z) ↔ ∀ i : ℕ, (c₀ i) (c₁ i) ≤ z :=
by
constructor <;> introv h
· apply h
· apply le_trans _ (h (max i j))
trans c₀ i (c₁ (max i j))
· apply (c₀ i).monotone
apply c₁.monotone
apply le_max_right
· apply c₀.monotone
apply le_max_left
