covering_disjoint_subtype — Mathlib

English

The coverings corresponding to distinct elements of the index, viewed via the subtype, are disjoint.

Русский

Покрытия, соответствующие различным элементам индекса, при просмотре через подтип, попарно несмежны.

LaTeX

$$$PairwiseDisjoint\\bigl(\\lambda x: h.covering x.val\\bigr).$$$

Lean4

theorem covering_disjoint_subtype : Pairwise (Disjoint on fun x : h.index => h.covering x) :=
  (pairwise_subtype_iff_pairwise_set _ _).2 h.covering_disjoint

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