fiber_none — Mathlib

English

The fiber over none is empty: RemoveNone.fiber none = empty set.

Русский

Фибра над none равна пустому множеству: RemoveNone.fiber none = ∅.

LaTeX

$$$ \operatorname{RemoveNone}.\operatorname{fiber}(\text{none}) = \emptyset$$$

Lean4

theorem fiber_none : RemoveNone.fiber (@none α) = ∅ :=
  by
  rw [Set.eq_empty_iff_forall_notMem]
  intro f hyp
  rw [RemoveNone.mem_fiber] at hyp
  rcases hyp with ⟨F, F_derangement, F_none, _⟩
  exact F_derangement none F_none

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