ite_mono — Mathlib

English

If s1 ⊆ s2 and s1' ⊆ s2', then t.ite s1 s1' ⊆ t.ite s2 s2'.

Русский

Если s1 ⊆ s2 и s1' ⊆ s2', то t.ite s1 s1' ⊆ t.ite s2 s2'.

LaTeX

$$$$ t.ite(s_1, s'_1) \subseteq t.ite(s_2, s'_2) \quad\text{whenever } s_1 \subseteq s_2 \text{ and } s'_1 \subseteq s'_2. $$$$

Lean4

theorem ite_mono (t : Set α) {s₁ s₁' s₂ s₂' : Set α} (h : s₁ ⊆ s₂) (h' : s₁' ⊆ s₂') : t.ite s₁ s₁' ⊆ t.ite s₂ s₂' :=
  union_subset_union (inter_subset_inter_left _ h) (inter_subset_inter_left _ h')

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