dom_prodLift — Mathlib

English

The domain of the product lift is the set of x with both f(x) and g(x) defined: (f.prodLift g).Dom = {x | (f x).Dom ∧ (g x).Dom}.

Русский

Область определения произведения lift состоит из тех x, для которых обе f(x) и g(x) определены.

LaTeX

$$$$ (f.prodLift g).Dom = \{ x \mid (f(x)).Dom \land (g(x)).Dom \}. $$$$

Lean4

@[simp]
theorem dom_prodLift (f : α →. β) (g : α →. γ) : (f.prodLift g).Dom = {x | (f x).Dom ∧ (g x).Dom} :=
  rfl

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