ext_iff — Mathlib

English

Under a fixed φ, if h1 holds, then σ1 = σ2 iff σ2 also holds the IsConj relation.

Русский

При фиксированном φ, если справедливо h1, тогда σ1 = σ2 тогда и только тогда σ2 также удовлетворяет IsConj.

LaTeX

$$For σ1, σ2: if IsConj φ σ1 then (σ1 = σ2 ↔ IsConj φ σ2)$$

Lean4

theorem ext_iff {σ₁ σ₂ : K ≃ₐ[k] K} (h₁ : IsConj φ σ₁) : σ₁ = σ₂ ↔ IsConj φ σ₂ :=
  ⟨fun e ↦ e ▸ h₁, h₁.ext⟩

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