realize_top — Mathlib

English

The top and bottom bounded formulas realize to True and False respectively; the realizations align with standard truth values.

Русский

Топовое и нижнее ограниченные формулы реализуются как True и False соответственно; реализации соответствуют обычным значениям истинности.

LaTeX

$$$ (⊤ : L.BoundedFormula α l).Realize v xs = True, \ (⊥ : L.BoundedFormula α l).Realize v xs = False $$$

Lean4

@[simp]
theorem realize_top : (⊤ : L.BoundedFormula α l).Realize v xs ↔ True := by simp [Top.top]

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