trans — Mathlib

English

If μ is inner regular with respect to p→q and q→q', then μ is inner regular with respect to p→q'.

Русский

Если μ имеет внутреннюю регулярность по переходам p→q и q→q', то она имеет регулярность по переходу p→q'.

LaTeX

$$$\text{If } InnerRegularWRT(\mu; p, q) \text{ and } InnerRegularWRT(\mu; q, q'), \; InnerRegularWRT(\mu; p, q').$$$

Lean4

theorem trans {q' : Set α → Prop} (H : InnerRegularWRT μ p q) (H' : InnerRegularWRT μ q q') : InnerRegularWRT μ p q' :=
  by
  intro U hU r hr
  rcases H' hU r hr with ⟨F, hFU, hqF, hF⟩; rcases H hqF _ hF with ⟨K, hKF, hpK, hrK⟩
  exact ⟨K, hKF.trans hFU, hpK, hrK⟩

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