realize_sup — Mathlib

English

For any formulas φ and ψ, the realization of their disjunction is equivalent to the disjunction of their realizations.

Русский

Для любых формул φ и ψ реализация дизъюнкции φ ⊔ ψ равна дизъюнкции реализаций φ и ψ.

LaTeX

$$$ (\phi \vee \psi)^M(v) \iff \phi^M(v) \lor \psi^M(v) $$$

Lean4

@[simp]
theorem realize_sup : (φ ⊔ ψ).Realize v ↔ φ.Realize v ∨ ψ.Realize v :=
  BoundedFormula.realize_sup

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