map_nontrivial — Mathlib

English

Let s be a finite set and f an embedding. Then (s.map f).Nontrivial is equivalent to s.Nontrivial.

Русский

Пусть s — конечное множество и f — инъекция. Тогда (s.map f).Nontrivial эквивалентно s.Nontrivial.

LaTeX

$$$(\\operatorname{image}(f,s)).\\mathrm{Nontrivial} \\iff s.\\mathrm{Nontrivial}$$$

Lean4

@[simp]
theorem map_nontrivial : (s.map f).Nontrivial ↔ s.Nontrivial :=
  mod_cast Set.image_nontrivial f.injective (s := s)

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