trans — Mathlib

English

If A is exposed to B and B is exposed to C, then A is exposed to C.

Русский

Если A экспонировано относительно B, а B — относительно C, тогда A экспонировано относительно C.

LaTeX

$$$$ IsExposed\ 𝕜\ A\ B \to IsExposed\ 𝕜\ B\ C \to IsExposed\ 𝕜\ A\ C. $$$$

Lean4

@[trans]
protected theorem trans (hAB : IsExtreme 𝕜 A B) (hBC : IsExtreme 𝕜 B C) : IsExtreme 𝕜 A C :=
  by
  refine ⟨hBC.subset.trans hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxC hx ↦ ?_⟩
  exact
    hBC.left_mem_of_mem_openSegment (hAB.left_mem_of_mem_openSegment hx₁A hx₂A (hBC.subset hxC) hx)
      (hAB.right_mem_of_mem_openSegment hx₁A hx₂A (hBC.subset hxC) hx) hxC hx

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