notMem_sigmaLift_of_ne_right — Mathlib

English

If the right indices differ, no element of sigmaLift f a b can have that right index; i.e., any element with b1 ≠ x1 is not in sigmaLift f a b.

Русский

Если правые индексы различны, никакой элемент sigmaLift f a b не имеет этого правого индекса; то есть любой элемент с b1 ≠ x1 не принадлежит sigmaLift f a b.

LaTeX

$$$$ x \notin \sigmaLift f a b \quad\text{if } b.1 \neq x.1 $$$$

Lean4

theorem notMem_sigmaLift_of_ne_right (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) {a : Sigma α} (b : Sigma β) {x : Sigma γ}
    (h : b.1 ≠ x.1) : x ∉ sigmaLift f a b := by
  rw [mem_sigmaLift]
  exact fun H => h H.snd.fst

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