elim

Mathlib.Data.Set.Pairwise.Basic

URI: https://scilib.ai/kg/mathlib#Set.PairwiseDisjoint.elim

English

If s is PairwiseDisjoint under f, and i, j ∈ s with notDisjoint f i and f j, then i = j.

Русский

Если s попарно непересекается относительно f и i, j ∈ s с неразличимыми образами, то i = j.

LaTeX

$$hs.elim hi hj h$$

Lean4

theorem elim (hs : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (h : ¬Disjoint (f i) (f j)) : i = j :=
  hs.eq hi hj h

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

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

Разделы

Аффилиация

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