ite_subset_union — Mathlib

English

The set chosen by a conditional (if P then s else s') is always contained in the union s ∪ s'.

Русский

Набор, получаемый через условие (если P тогда s иначе s'), всегда содержится в объединении s ∪ s'.

LaTeX

$$$ \\mathrm{ite}\\, P\\, s\\, s' \\subseteq s \\cup s' $$$

Lean4

theorem ite_subset_union (s s' : Finset α) (P : Prop) [Decidable P] : ite P s s' ⊆ s ∪ s' :=
  ite_le_sup s s' P

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