tr_eval_dom — Mathlib

English

For any a1,a2, the domain of eval f2 a2 is equivalent to the domain of eval f1 a1 under the respect condition.

Русский

Для любых a1,a2 области определения eval f2 a2 совпадают с eval f1 a1 под условием уважительности.

LaTeX

$$$\\forall {f_1 f_2 tr} (H : Respects f_1 f_2 tr) \\forall {a_1 a_2},\\ (eval f_2 a_2).\\mathrm{Dom} \\leftrightarrow (eval f_1 a_1).\\mathrm{Dom}$$$

Lean4

theorem tr_eval_dom {σ₁ σ₂ f₁ f₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ a₂} (aa : tr a₁ a₂) :
    (eval f₂ a₂).Dom ↔ (eval f₁ a₁).Dom :=
  ⟨fun h ↦
    let ⟨_, _, h, _⟩ := tr_eval_rev H aa ⟨h, rfl⟩
    h,
    fun h ↦
    let ⟨_, _, h, _⟩ := tr_eval H aa ⟨h, rfl⟩
    h⟩

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