eq_iff — Mathlib

English

Equality of lifts is characterized by carrier equality and embedding compatibility.

Русский

Равенство подполей характеризуется равенством носителей и совместимостью вложений.

LaTeX

$$$L_1 = L_2 \\iff \\exists h : L_1.carrier = L_2.carrier, L_2.emb.comp (inclusion h.le) = L_1.emb$$$

Lean4

theorem eq_iff : L₁ = L₂ ↔ ∃ h : L₁.carrier = L₂.carrier, L₂.emb.comp (inclusion h.le) = L₁.emb :=
  by
  rw [eq_iff_le_carrier_eq, le_iff]
  exact ⟨fun h ↦ ⟨h.2, h.1.2⟩, fun h ↦ ⟨⟨h.1.le, h.2⟩, h.1⟩⟩

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