ite_mem — Mathlib

English

Let p be a decidable proposition, a,b ∈ α, and s a set in α. Then (if p then a else b) ∈ s if and only if (p implies a ∈ s) and (not p implies b ∈ s).

Русский

Пусть p — решаемое proposition, a,b ∈ α, и s ⊆ α. Тогда (если p истина, то a ∈ s, иначе b ∈ s) эквивалентно (p ⇒ a ∈ s) и (¬p ⇒ b ∈ s).

LaTeX

$$$ (\operatorname{ite}(p,a,b)) \in s \; \Longleftrightarrow \; (p \rightarrow a \in s) \land (\neg p \rightarrow b \in s) $$$

Lean4

theorem ite_mem {a b : α} {s : β} : (if p then a else b) ∈ s ↔ (p → a ∈ s) ∧ (¬p → b ∈ s) :=
  dite_mem

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