English
If the first and second family components are monotone with respect to inclusion (f1 ⊆ f1', f2 ⊆ f2', g1 ⊆ g1', g2 ⊆ g2'), then for all a,b the lifting sumLexLift(f1,f2,g1,g2) a b is contained in sumLexLift(f1',f2',g1',g2') a b.
Русский
Пусть f1 ⊆ f1', f2 ⊆ f2', g1 ⊆ g1', g2 ⊆ g2'. Тогда для любых a,b множество sumLexLift(f1,f2,g1,g2) a b содержится в sumLexLift(f1',f2',g1',g2') a b.
LaTeX
$$$\mathrm{sumLexLift}(f_1,f_2,g_1,g_2)\ a\ b \subseteq \mathrm{sumLexLift}(f_1',f_2',g_1',g_2')\ a\ b$$$
Lean4
theorem sumLexLift_mono (hf₁ : ∀ a b, f₁ a b ⊆ f₁' a b) (hf₂ : ∀ a b, f₂ a b ⊆ f₂' a b) (hg₁ : ∀ a b, g₁ a b ⊆ g₁' a b)
(hg₂ : ∀ a b, g₂ a b ⊆ g₂' a b) (a : α₁ ⊕ α₂) (b : β₁ ⊕ β₂) :
sumLexLift f₁ f₂ g₁ g₂ a b ⊆ sumLexLift f₁' f₂' g₁' g₂' a b :=
by
cases a <;> cases b
exacts [map_subset_map.2 (hf₁ _ _), disjSum_mono (hg₁ _ _) (hg₂ _ _), Subset.rfl, map_subset_map.2 (hf₂ _ _)]
