trans_eq_none — Mathlib

English

The composite is none exactly when, for all b,c, either b is not in f a or c is not in g b.

Русский

Композиция равна none тогда и только тогда, когда для всех b,c верно, что либо b не принадлежит f a, либо c не принадлежит g b.

LaTeX

$$$$ f.trans g a = \\text{none} \\iff \\forall b c, b \\notin f a \\lor c \\notin g b. $$$$

Lean4

theorem trans_eq_none (f : α ≃. β) (g : β ≃. γ) (a : α) : f.trans g a = none ↔ ∀ b c, b ∉ f a ∨ c ∉ g b :=
  by
  simp only [eq_none_iff_forall_not_mem, mem_trans, imp_iff_not_or.symm]
  push_neg
  exact forall_swap

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