eq_of_mem_slice

Mathlib.Data.Finset.Slice

URI: https://scilib.ai/kg/mathlib#Finset.eq_of_mem_slice

English

If A belongs to two slices with radii r1 and r2, then r1 = r2.

Русский

Если A принадлежит двум срезам с размерностями r1 и r2, то r1 = r2.

LaTeX

$$$ A \in 𝒜_{r_1} \land A \in 𝒜_{r_2} \Rightarrow r_1 = r_2 $$$

Lean4

theorem eq_of_mem_slice (h₁ : A ∈ 𝒜 #r₁) (h₂ : A ∈ 𝒜 #r₂) : r₁ = r₂ :=
  (sized_slice h₁).symm.trans <| sized_slice h₂

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru