disjSum_ssubset_disjSum_of_subset_of_ssubset

English

Monotone right 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 \subseteq s_2 \land t_1 \subset t_2 \Rightarrow s_1.disjSum t_1 \subset s_2.disjSum t_2 $$$

Lean4

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

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