sumLift₂_mono — Mathlib

English

If f1 ≤ g1 and f2 ≤ g2 componentwise, then sumLift₂ f1 f2 ≤ sumLift₂ g1 g2.

Русский

Если f1 ⊆ g1 и f2 ⊆ g2 по компонентам, то sumLift₂ f1 f2 ⊆ sumLift₂ g1 g2.

LaTeX

$$sumLift₂_mono (h1) (h2) : ∀ a b, sumLift₂ f1 f2 a b ⊆ sumLift₂ g1 g2 a b$$

Lean4

theorem sumLift₂_mono (h₁ : ∀ a b, f₁ a b ⊆ g₁ a b) (h₂ : ∀ a b, f₂ a b ⊆ g₂ a b) :
    ∀ a b, sumLift₂ f₁ f₂ a b ⊆ sumLift₂ g₁ g₂ a b
  | inl _, inl _ => map_subset_map.2 (h₁ _ _)
  | inl _, inr _ => Subset.rfl
  | inr _, inl _ => Subset.rfl
  | inr _, inr _ => map_subset_map.2 (h₂ _ _)

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