English
If f is monotone in its index, then the bounded sup-subtraction of a nadd b equals the maximum of the two corresponding subtractions — one varying the first argument and one the second.
Русский
Если f монотонно по инексу, то \mathrm{blsub}(a \nadd b) равно максимуму из двух соответствующих подвычетов: по первому и по второму аргументу.
LaTeX
$$$\forall a,b \; \forall f\; (\forall i,j, i \le j \Rightarrow f(i,hi) \le f(j,hj)) \, \Rightarrow\; (a\nadd b).blsub f = \max\left( a.blsub (\lambda a' ha' \mapsto f(a' \# b)) ,\; b.blsub (\lambda b' hb' \mapsto f(a \# b')) \right)$$$
Lean4
@[deprecated "blsub will soon be deprecated" (since := "2024-11-18")]
theorem blsub_nadd_of_mono {f : ∀ c < a ♯ b, Ordinal.{max u v}} (hf : ∀ {i j} (hi hj), i ≤ j → f i hi ≤ f j hj) :
blsub.{u, v} _ f =
max (blsub.{u, v} a fun a' ha' => f (a' ♯ b) <| nadd_lt_nadd_right ha' b)
(blsub.{u, v} b fun b' hb' => f (a ♯ b') <| nadd_lt_nadd_left hb' a) :=
by
apply (blsub_le_iff.2 fun i h => _).antisymm (max_le _ _)
· intro i h
rcases lt_nadd_iff.1 h with (⟨a', ha', hi⟩ | ⟨b', hb', hi⟩)
· exact lt_max_of_lt_left ((hf h (nadd_lt_nadd_right ha' b) hi).trans_lt (lt_blsub _ _ ha'))
· exact lt_max_of_lt_right ((hf h (nadd_lt_nadd_left hb' a) hi).trans_lt (lt_blsub _ _ hb'))
all_goals
apply blsub_le_of_brange_subset.{u, u, v}
rintro c ⟨d, hd, rfl⟩
apply mem_brange_self
