ite — Mathlib

English

ITE for sets: define t.ite s s' as (s ∩ t) ∪ (s' \ t).

Русский

Определение разности условий для множеств: t.ite s s' = (s ∩ t) ∪ (s' \ t).

LaTeX

$$$$ \text{Set}.ite(t, s, s') = (s \cap t) \cup (s' \setminus t). $$$$

Lean4

/-- `ite` for sets: `Set.ite t s s' ∩ t = s ∩ t`, `Set.ite t s s' ∩ tᶜ = s' ∩ tᶜ`.
Defined as `s ∩ t ∪ s' \ t`. -/
protected def ite (t s s' : Set α) : Set α :=
  s ∩ t ∪ s' \ t

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