familyOfElements_compatible — Mathlib

English

From hx (Compatible P π x), one can form hx.familyOfElements, and this family is compatible in the sense hx.familyOfElements.Compatible.

Русский

Из hx (Compatible P π x) получаем hx.familyOfElements, и эта семья совместима в смысле hx.familyOfElements.Compatible.

LaTeX

$$hx.familyOfElements.Compatible$$

Lean4

theorem familyOfElements_compatible : hx.familyOfElements.Compatible :=
  by
  rintro Y₁ Y₂ Z g₁ g₂ f₁ f₂ ⟨i⟩ ⟨j⟩ hgf
  simp [hx i j Z g₁ g₂ hgf]

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