elim'

Mathlib.Data.Set.Pairwise.Basic

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

← MathLib Explorer

English

If s is PairwiseDisjoint under f, then for i,j in s, if f i ⊓ f j ≠ ⊥, then i = j.

Русский

Если s попарно непересекается относительно f, то для любых i,j∈s, если f i ⊓ f j ≠ ⊥, то i = j.

LaTeX

$$hs.elim' hi hj h$$

Lean4

theorem elim' (hs : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (h : f i ⊓ f j ≠ ⊥) : i = j :=
  (hs.elim hi hj) fun hij => h hij.eq_bot

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

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

Разделы

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

Аффилиация

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