disjoint_coe — Mathlib

English

Disjointness is preserved by the coercion: Disjoint(a.val, b.val) iff Disjoint(a, b).

Русский

Несовместимость сохраняется при отображении через включение: Disjoint(a.val, b.val) эквивалентно Disjoint(a, b).

LaTeX

$$$\forall a,b\in \mathrm{Complementeds}(\alpha),\ Disjoint(a.\mathrm{val}, b.\mathrm{val}) \iff Disjoint(a,b).$$$

Lean4

@[simp, norm_cast]
theorem disjoint_coe : Disjoint (a : α) b ↔ Disjoint a b := by
  rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]

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