comap_const_of_notMem — Mathlib

English

If x is not contained in a given t ∈ g, the comap becomes bottom.

Русский

Если x не содержится в некотором m из g, то comap становится ⊥.

LaTeX

$$$ \exists t \in g, x \notin t \Rightarrow \mathrm{comap}(\lambda -,x) g = \bot $$$

Lean4

theorem comap_const_of_notMem {x : β} (ht : t ∈ g) (hx : x ∉ t) : comap (fun _ : α => x) g = ⊥ :=
  empty_mem_iff_bot.1 <| mem_comap'.2 <| mem_of_superset ht fun _ hx' _ h => hx <| h.symm ▸ hx'

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