liftCover_of_mem — Mathlib

English

If x ∈ S_i, then liftCover S f hf hS x = f_i ⟨x, hx⟩. (Alternative form of the same compatibility.)

Русский

Если x ∈ S_i, тогда liftCover S f hf hS x = f_i ⟨x, hx⟩. (Альтернативная форма той же совместимости.)

LaTeX

$$$\forall i\in ι,\; \forall x\in S_i:\ liftCover(S,f,hf,hS)(x) = f_i(\langle x, hx\rangle).$$$

Lean4

theorem liftCover_of_mem {i : ι} {x : α} (hx : (x : α) ∈ S i) : liftCover S f hf hS x = f i ⟨x, hx⟩ :=
  iUnionLift_of_mem (⟨x, trivial⟩ : { _z // True }) hx

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