English
If a family {f} is pairwise disjoint and e: α → β with a factorization through e, then the extended family extend e f ⊥ is pairwise disjoint.
Русский
Если множество {f} попарно непересекается и e: α → β с факторизацией через e, тогда расширенная семейство extend e f ⊥ попарно непересекается.
LaTeX
$$$ \text{Pairwise}(\operatorname{Disjoint} \circ \operatorname{extend}(e,f,\bot)) $$$
Lean4
theorem disjoint_extend_bot [PartialOrder γ] [OrderBot γ] {e : α → β} {f : α → γ} (hf : Pairwise (Disjoint on f))
(he : FactorsThrough f e) : Pairwise (Disjoint on extend e f ⊥) :=
by
intro b₁ b₂ hne
rcases em (∃ a₁, e a₁ = b₁) with ⟨a₁, rfl⟩ | hb₁
· rcases em (∃ a₂, e a₂ = b₂) with ⟨a₂, rfl⟩ | hb₂
· simpa only [onFun, he.extend_apply] using hf (ne_of_apply_ne e hne)
· simpa only [onFun, extend_apply' _ _ _ hb₂] using disjoint_bot_right
· simpa only [onFun, extend_apply' _ _ _ hb₁] using disjoint_bot_left
