English
If for every index i and all a in α_i and b in β_i we have f a b ⊆ g a b, then for all a : Σ i, α_i and b : Σ i, β_i we have sigmaLift f a b ⊆ sigmaLift g a b.
Русский
Если для каждого индекса i и всех a в α_i и b в β_i выполнено f a b ⊆ g a b, то для любых a : Σ i, α_i и b : Σ i, β_i выполняется sigmaLift f a b ⊆ sigmaLift g a b.
LaTeX
$$$\\bigl(\\forall i,\\forall a\\in \\alpha_i,\\forall b\\in \\beta_i, f(a,b) \\subseteq g(a,b)\\bigr) \\Rightarrow \\forall a: \\sum_{i} \\alpha_i, \\forall b: \\sum_{i} \\beta_i,\\ sigmaLift f\\,a\\,b \\subseteq sigmaLift g\\,a\\,b.$$$
Lean4
theorem sigmaLift_mono (h : ∀ ⦃i⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b) (a : Σ i, α i) (b : Σ i, β i) :
sigmaLift f a b ⊆ sigmaLift g a b := by
rintro x hx
rw [mem_sigmaLift] at hx ⊢
obtain ⟨ha, hb, hx⟩ := hx
exact ⟨ha, hb, h hx⟩
