subtypeDomain_eq_iff_forall — Mathlib

English

Two subtypeDomain restrictions are equal iff the functions agree on every p-element.

Русский

Две ограниченные подтип-домены равны тогда и только тогда, когда функции совпадают на всех элементах, удовлетворяющих p.

LaTeX

$$$$ f.subtypeDomain p = g.subtypeDomain p \\iff \\forall x, p x \\to f x = g x. $$$$

Lean4

theorem subtypeDomain_eq_iff_forall {f g : α →₀ M} : f.subtypeDomain p = g.subtypeDomain p ↔ ∀ x, p x → f x = g x := by
  simp_rw [DFunLike.ext_iff, subtypeDomain_apply, Subtype.forall]

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