subset_ite — Mathlib

English

For sets t, s, s', u, we have u ⊆ t.ite s s' iff (u ∩ t) ⊆ s and (u \ t) ⊆ s'.

Русский

Для множеств t, s, s', u выполнено: u ⊆ t.ite s s' эквивалентно (u ∩ t) ⊆ s и u \ t ⊆ s'.

LaTeX

$$$ u \subseteq t.ite s s' \iff (u \cap t) \subseteq s \land (u \setminus t) \subseteq s' $$$

Lean4

theorem subset_ite {t s s' u : Set α} : u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s' :=
  by
  simp only [subset_def, ← forall_and]
  refine forall_congr' fun x => ?_
  by_cases hx : x ∈ t <;> simp [*, Set.ite]

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