subtypeSubtypeEquivSubtypeInter — Mathlib

English

A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates: { x : Subtype p // q x.1 } ≃ Subtype (fun x => p x ∧ q x).

Русский

Подтип подтипа эквивалентен подтипу элементов, удовлетворяющих обоим предикатам: { x : Subtype p // q x.1 } ≃ { x : α | p x ∧ q x }.

LaTeX

$$$\\{ x : \\text{Subtype } p \\;\\mid\\; q x.1 \\} \\simeq \\{ x : \\alpha \\mid p x \\land q x \\}$$$

Lean4

/-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. -/
@[simps!]
def subtypeSubtypeEquivSubtypeInter {α : Type u} (p q : α → Prop) :
    { x : Subtype p // q x.1 } ≃ Subtype fun x => p x ∧ q x :=
  (subtypeSubtypeEquivSubtypeExists p _).trans <| subtypeEquivRight fun x => @exists_prop (q x) (p x)

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