emb_zero

Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

URI: https://scilib.ai/kg/mathlib#OrderedFinpartition.emb_zero

← MathLib Explorer

English

If i ≠ j then c.emb i a ≠ c.emb j b.

Русский

Если i ≠ j, то c.emb i a ≠ c.emb j b.

LaTeX

$$$\\forall i,j:\\mathrm{Fin}(c.length),\\ i \\neq j \\Rightarrow \\forall a,b,\\; c.emb i a \\neq c.emb j b$$$

Lean4

theorem emb_zero [NeZero n] : c.emb (c.index 0) 0 = 0 :=
  by
  apply le_antisymm _ (Fin.zero_le _)
  conv_rhs => rw [← c.emb_invEmbedding 0]
  apply (c.emb_strictMono _).monotone (Fin.zero_le _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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