mlieBracketWithin_congr' — Mathlib

English

Variant: if V₁ and W₁ coincide with V and W on s, and x ∈ s, then the bracket values equal.

Русский

Вариант: если V₁ совпадает с V и W₁ с W на s и x ∈ s, тогда значения скобки равны.

LaTeX

$$$hV : EqOn V₁ V s \to hVx : V₁ x = V x \to hW : EqOn W₁ W s \to hWx : W₁ x = W x \Rightarrow mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x$$$

Lean4

/-- Version of `mlieBracketWithin_congr` in which one assumes that the point belongs to the
given set. -/
theorem mlieBracketWithin_congr' (hV : EqOn V₁ V s) (hW : EqOn W₁ W s) (hx : x ∈ s) :
    mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x :=
  mlieBracketWithin_congr hV (hV hx) hW (hW hx)

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