convexJoin_mono — Mathlib

English

If s1 ⊆ s2 and t1 ⊆ t2, then convexJoin 𝕜 s1 t1 ⊆ convexJoin 𝕜 s2 t2.

Русский

Если s1 ⊆ s2 и t1 ⊆ t2, то convexJoin 𝕜 s1 t1 ⊆ convexJoin 𝕜 s2 t2.

LaTeX

$$$ s_1 \subseteq s_2 \rightarrow t_1 \subseteq t_2 \rightarrow convexJoin 𝕜 s_1 t_1 \subseteq convexJoin 𝕜 s_2 t_2 $$$

Lean4

theorem convexJoin_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : convexJoin 𝕜 s₁ t₁ ⊆ convexJoin 𝕜 s₂ t₂ :=
  biUnion_mono hs fun _ _ => biUnion_subset_biUnion_left ht

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