mem_ite — Mathlib

English

Membership in an ite expression is equivalent to a pair of universal memberships: (a ∈ ite p s t) ↔ (p → a ∈ s) ∧ (¬p → a ∈ t).

Русский

Принадлежность к выражению ite эквивалентна паре всеобъемлющих принадлежностей: (a ∈ ite p s t) ↔ (p → a ∈ s) ∧ (¬p → a ∈ t).

LaTeX

$$$\big(a \in \text{ite } p\ s\ t\big) \iff (p \to a \in s) \land (\lnot p \to a \in t)$$$

Lean4

theorem mem_ite {a : α} {s t : β} : (a ∈ if p then s else t) ↔ (p → a ∈ s) ∧ (¬p → a ∈ t) :=
  mem_dite

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