trans_single_of_eq_none — Mathlib

English

If f.symm b = none, then f.trans (single b c) = ⊥.

Русский

Если f.symm b = None, то f.trans (single b c) = ⊥.

LaTeX

$$f.symm b = None \Rightarrow f.trans (single b c) = \bot$$

Lean4

theorem trans_single_of_eq_none {b : β} (c : γ) {f : δ ≃. β} (h : f.symm b = none) : f.trans (single b c) = ⊥ :=
  by
  ext
  simp only [eq_none_iff_forall_not_mem, Option.mem_def, f.eq_some_iff] at h
  dsimp [PEquiv.trans, single]
  simp only [bind_eq_some_iff, iff_false, not_exists, not_and, reduceCtorEq]
  intros
  split_ifs <;> simp_all

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