injective_coe — Mathlib

English

Two boxes have the same underlying set iff they are equal.

Русский

Две коробки имеют одно и то же базовое множество тогда и только тогда, когда они равны.

LaTeX

$$$ (I.toSet = J.toSet) \\iff I = J $$$

Lean4

theorem injective_coe : Injective ((↑) : Box ι → Set (ι → ℝ)) :=
  by
  rintro ⟨l₁, u₁, h₁⟩ ⟨l₂, u₂, h₂⟩ h
  simp only [Subset.antisymm_iff, coe_subset_coe, le_iff_bounds] at h
  congr
  exacts [le_antisymm h.2.1 h.1.1, le_antisymm h.1.2 h.2.2]

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