of_isAtom_coe_Iic — Mathlib

English

If a is an atom in Set.Iic x, then its underlying element a.val is an atom in α.

Русский

Если a является атомом в Set.Iic x, то его базовый элемент a.val является атомом в α.

LaTeX

$$$IsAtom(a) \\rightarrow IsAtom(a.\\text{val}).$$$

Lean4

theorem of_isAtom_coe_Iic {a : Set.Iic x} (ha : IsAtom a) : IsAtom (a : α) :=
  ⟨fun con => ha.1 (Subtype.ext con), fun b hba => Subtype.mk_eq_mk.1 (ha.2 ⟨b, hba.le.trans a.prop⟩ hba)⟩

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