eq_iff_le_carrier_eq — Mathlib

English

Equality of two lifts is equivalent to a pair consisting of carrier equality and a compatibility of embeddings.

Русский

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

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_le_carrier_eq : L₁ = L₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier = L₂.carrier :=
  ⟨fun eq ↦ ⟨eq.le, congr_arg _ eq⟩, fun ⟨le, eq⟩ ↦ le.antisymm ⟨eq.ge, fun x ↦ (le.2 ⟨x, _⟩).symm⟩⟩

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