congr — Mathlib

English

If t is eventually measurable and s ≡_l t, then s is eventually measurable.

Русский

Если t в Ultimately измеримо, и s эквивалентно t по l, то s тоже измеримо.

LaTeX

$$$\text{ht} : \text{EventuallyMeasurableSet}(m,l,t) \land s =^l t \;\Rightarrow\; \text{EventuallyMeasurableSet}(m,l,s).$$$

Lean4

/-- A set which is `EventuallyEq` to an `EventuallyMeasurableSet`
is an `EventuallyMeasurableSet`. -/
theorem congr (ht : EventuallyMeasurableSet m l t) (hst : s =ᶠ[l] t) : EventuallyMeasurableSet m l s :=
  by
  rcases ht with ⟨t', ht', htt'⟩
  exact ⟨t', ht', hst.trans htt'⟩

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