disjSum_ssubset_disjSum_of_ssubset_of_subset

English

Monotone left with subset relation: if s1 ⊂ s2 and t1 ⊆ t2 then s1.disjSum t1 ⊂ s2.disjSum t2.

Русский

Монотонность слева при частичном порядке: если s1 ⊂ s2 и t1 ⊆ t2, то s1.disjSum t1 ⊂ s2.disjSum t2.

LaTeX

$$$ s_1 \subset s_2 \land t_1 \subseteq t_2 \Rightarrow s_1.disjSum t_1 \subset s_2.disjSum t_2 $$$

Lean4

theorem disjSum_ssubset_disjSum_of_ssubset_of_subset (hs : s₁ ⊂ s₂) (ht : t₁ ⊆ t₂) : s₁.disjSum t₁ ⊂ s₂.disjSum t₂ :=
  val_lt_iff.1 <| disjSum_lt_disjSum_of_lt_of_le (val_lt_iff.2 hs) (val_le_iff.2 ht)

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