@[trans]
Implication →
is transitive. If P → Q
and Q → R
then P → R
.
theorem
trans_rel_left
{α : Sort u}
{a b c : α}
(r : α → α → Prop)
(h₁ : r a b)
(h₂ : b = c) :
r a c
theorem
trans_rel_right
{α : Sort u}
{a b c : α}
(r : α → α → Prop)
(h₁ : a = b)
(h₂ : r b c) :
r a c
@[trans]
@[trans]
theorem
eq_rec_heq
{α : Sort u}
{φ : α → Sort v}
{a a' : α}
(h : a = a')
(p : φ a) :
h.rec_on p == p
theorem
heq_of_eq_rec_left
{α : Sort u}
{φ : α → Sort v}
{a a' : α}
{p₁ : φ a}
{p₂ : φ a'}
(e : a = a')
(h₂ : e.rec_on p₁ = p₂) :
p₁ == p₂
theorem
heq_of_eq_rec_right
{α : Sort u}
{φ : α → Sort v}
{a a' : α}
{p₁ : φ a}
{p₂ : φ a'}
(e : a' = a)
(h₂ : p₁ = e.rec_on p₂) :
p₁ == p₂
theorem
eq_rec_compose
{α β φ : Sort u}
(p₁ : β = φ)
(p₂ : α = β)
(a : α) :
p₁.rec_on (p₂.rec_on a) = _.rec_on a
- mp : a → b
- mpr : b → a
iff P Q
, with notation P ↔ Q
, is the proposition asserting that P
and Q
are equivalent,
that is, have the same truth value.
Instances for iff
- intro : ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
The existential quantifier.
To prove a goal of the form ⊢ ∃ x, p x
, you can provide a witness y
with the tactic existsi y
.
If you are working in a project that depends on mathlib, then we recommend the use
tactic
instead.
You'll then be left with the goal ⊢ p y
.
To extract a witness x
and proof hx : p x
from a hypothesis h : ∃ x, p x
,
use the tactic cases h with x hx
. See also the mathlib tactics obtain
and rcases
.
Instances for Exists
- exists_prop_decidable
- list.decidable_bex
- option.decidable_exists_mem
- bool.decidable_exists_bool
- nat.decidable_exists_lt
- nat.decidable_exists_le
- multiset.decidable_dexists_multiset
- finset.decidable_dexists_finset
- finset.decidable_exists_of_decidable_subsets
- finset.decidable_exists_of_decidable_ssubsets
- fintype.decidable_exists_fintype
- pnat.decidable_pred_exists_nat
theorem
exists.elim
{α : Sort u}
{p : α → Prop}
{b : Prop}
(h₁ : ∃ (x : α), p x)
(h₂ : ∀ (a : α), p a → b) :
b
Equations
- exists_unique p = ∃ (x : α), p x ∧ ∀ (y : α), p y → y = x
theorem
exists_unique.intro
{α : Sort u}
{p : α → Prop}
(w : α)
(h₁ : p w)
(h₂ : ∀ (y : α), p y → y = w) :
∃! (x : α), p x
theorem
exists_unique.elim
{α : Sort u}
{p : α → Prop}
{b : Prop}
(h₂ : ∃! (x : α), p x)
(h₁ : ∀ (x : α), p x → (∀ (y : α), p y → y = x) → b) :
b
theorem
exists_unique_of_exists_of_unique
{α : Sort u}
{p : α → Prop}
(hex : ∃ (x : α), p x)
(hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) :
∃! (x : α), p x
theorem
unique_of_exists_unique
{α : Sort u}
{p : α → Prop}
(h : ∃! (x : α), p x)
{y₁ y₂ : α}
(py₁ : p y₁)
(py₂ : p y₂) :
y₁ = y₂
theorem
forall_congr
{α : Sort u}
{p q : α → Prop}
(h : ∀ (a : α), p a ↔ q a) :
(∀ (a : α), p a) ↔ ∀ (a : α), q a
theorem
exists_imp_exists
{α : Sort u}
{p q : α → Prop}
(h : ∀ (a : α), p a → q a)
(p_1 : ∃ (a : α), p a) :
∃ (a : α), q a
theorem
exists_unique_congr
{α : Sort u}
{p₁ p₂ : α → Prop}
(h : ∀ (x : α), p₁ x ↔ p₂ x) :
exists_unique p₁ ↔ ∃! (x : α), p₂ x
Equations
- decidable.to_bool p = h.cases_on (λ (h₁ : ¬p), bool.ff) (λ (h₂ : p), bool.tt)
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
def
decidable.rec_on_true
{p : Prop}
[h : decidable p]
{h₁ : p → Sort u}
{h₂ : ¬p → Sort u}
(h₃ : p)
(h₄ : h₁ h₃) :
h.rec_on h₂ h₁
Equations
- decidable.rec_on_true h₃ h₄ = h.rec_on (λ (h : ¬p), false.rec ((decidable.is_false h).rec_on h₂ h₁) _) (λ (h : p), h₄)
def
decidable.rec_on_false
{p : Prop}
[h : decidable p]
{h₁ : p → Sort u}
{h₂ : ¬p → Sort u}
(h₃ : ¬p)
(h₄ : h₂ h₃) :
h.rec_on h₂ h₁
Equations
- decidable.rec_on_false h₃ h₄ = h.rec_on (λ (h : ¬p), h₄) (λ (h : p), false.rec ((decidable.is_true h).rec_on h₂ h₁) _)
Equations
Equations
- decidable_of_decidable_of_iff hp h = dite p (λ (hp : p), decidable.is_true _) (λ (hp : ¬p), decidable.is_false _)
Equations
@[protected, instance]
Equations
- and.decidable = dite p (λ (hp : p), dite q (λ (hq : q), decidable.is_true _) (λ (hq : ¬q), decidable.is_false _)) (λ (hp : ¬p), decidable.is_false _)
@[protected, instance]
Equations
- or.decidable = dite p (λ (hp : p), decidable.is_true _) (λ (hp : ¬p), dite q (λ (hq : q), decidable.is_true _) (λ (hq : ¬q), decidable.is_false _))
@[protected, instance]
Equations
- not.decidable = dite p (λ (hp : p), decidable.is_false _) (λ (hp : ¬p), decidable.is_true hp)
@[protected, instance]
Equations
- implies.decidable = dite p (λ (hp : p), dite q (λ (hq : q), decidable.is_true _) (λ (hq : ¬q), decidable.is_false _)) (λ (hp : ¬p), decidable.is_true _)
@[protected, instance]
Equations
- iff.decidable = dite p (λ (hp : p), dite q (λ (hq : q), decidable.is_true _) (λ (hq : ¬q), decidable.is_false _)) (λ (hp : ¬p), dite q (λ (hq : q), decidable.is_false _) (λ (hq : ¬q), decidable.is_true _))
@[protected, instance]
Equations
- xor.decidable = dite p (λ (hp : p), dite q (λ (hq : q), decidable.is_false _) (λ (hq : ¬q), decidable.is_true _)) (λ (hp : ¬p), dite q (λ (hq : q), decidable.is_true _) (λ (hq : ¬q), decidable.is_false _))
@[protected, instance]
def
exists_prop_decidable
{p : Prop}
(P : p → Prop)
[Dp : decidable p]
[DP : Π (h : p), decidable (P h)] :
decidable (∃ (h : p), P h)
Equations
- exists_prop_decidable P = dite p (λ (h : p), decidable_of_decidable_of_iff (DP h) _) (λ (h : ¬p), decidable.is_false _)
@[protected, instance]
def
forall_prop_decidable
{p : Prop}
(P : p → Prop)
[Dp : decidable p]
[DP : Π (h : p), decidable (P h)] :
decidable (∀ (h : p), P h)
Equations
- forall_prop_decidable P = dite p (λ (h : p), decidable_of_decidable_of_iff (DP h) _) (λ (h : ¬p), decidable.is_true _)
@[protected, instance]
Equations
Equations
- is_dec_refl p = ∀ (x : α), p x x = bool.tt
@[protected, instance]
def
decidable_eq_of_bool_pred
{α : Sort u}
{p : α → α → bool}
(h₁ : is_dec_eq p)
(h₂ : is_dec_refl p) :
Equations
- decidable_eq_of_bool_pred h₁ h₂ = λ (x y : α), dite (p x y = bool.tt) (λ (hp : p x y = bool.tt), decidable.is_true _) (λ (hp : ¬p x y = bool.tt), decidable.is_false _)
theorem
decidable_eq_inl_refl
{α : Sort u}
[h : decidable_eq α]
(a : α) :
h a a = decidable.is_true _
theorem
decidable_eq_inr_neg
{α : Sort u}
[h : decidable_eq α]
{a b : α}
(n : a ≠ b) :
h a b = decidable.is_false n
@[class]
- default : α
Instances of this typeclass
- unique.inhabited
- prop.inhabited
- pi.inhabited
- bool.inhabited
- true.inhabited
- prod.inhabited
- nat.inhabited
- list.inhabited
- char.inhabited
- string.inhabited
- sum.inhabited_left
- sum.inhabited_right
- name.inhabited
- option.inhabited
- options.inhabited
- format.inhabited
- level.inhabited
- expr.inhabited
- environment.implicit_infer_kind.inhabited
- environment.inhabited
- local_context.inhabited
- occurrences.inhabited
- punit.inhabited
- json.inhabited
- sort.inhabited
- sort.inhabited'
- psum.inhabited_left
- psum.inhabited_right
- vm_decl_kind.inhabited
- vm_obj_kind.inhabited
- tactic.new_goals.inhabited
- tactic.transparency.inhabited
- tactic.apply_cfg.inhabited
- smt_pre_config.inhabited
- ematch_config.inhabited
- cc_config.inhabited
- smt_config.inhabited
- rsimp.config.inhabited
- tactic.dunfold_config.inhabited
- tactic.dsimp_config.inhabited
- tactic.unfold_proj_config.inhabited
- tactic.simp_intros_config.inhabited
- tactic.delta_config.inhabited
- tactic.simp_config.inhabited
- tactic.rewrite_cfg.inhabited
- interactive.loc.inhabited
- tactic.unfold_config.inhabited
- param_info.inhabited
- subsingleton_info.inhabited
- fun_info.inhabited
- format.color.inhabited
- pos.inhabited
- environment.projection_info.inhabited
- reducibility_hints.inhabited
- congr_arg_kind.inhabited
- ulift.inhabited
- plift.inhabited
- string_imp.inhabited
- string.iterator_imp.inhabited
- rbnode.color.inhabited
- ordering.inhabited
- unification_constraint.inhabited
- pprod.inhabited
- unification_hint.inhabited
- doc_category.inhabited
- tactic_doc_entry.inhabited
- bin_tree.inhabited
- unsigned.inhabited
- string.iterator.inhabited
- rbnode.inhabited
- rbtree.inhabited
- rbmap.inhabited
- binder_info.inhabited
- binder.inhabited
- tactic.goal.inhabited
- tactic.proof_state.inhabited
- to_additive.value_type.inhabited
- native.rb_set.inhabited
- native.rb_map.inhabited
- native.rb_lmap.inhabited
- name_set.inhabited
- name_map.inhabited
- lint_verbosity.inhabited
- tactic.rcases_patt.inhabited
- tactic.explode.status.inhabited
- tactic.explode.entries.inhabited
- auto.auto_config.inhabited
- auto.case_option.inhabited
- tactic.itauto.and_kind.inhabited
- tactic.itauto.prop.inhabited
- tactic.itauto.proof.inhabited
- norm_cast.label.inhabited
- norm_cast.norm_cast_cache.inhabited
- projection_data.inhabited
- simps_cfg.inhabited
- functor.const.inhabited
- functor.add_const.inhabited
- functor.comp.inhabited
- applicative_transformation.inhabited
- tactic.suggest.head_symbol_match.inhabited
- quot.inhabited
- quotient.inhabited
- trunc.inhabited
- sigma.inhabited
- psigma.inhabited
- fin.inhabited
- inhabited_fin_one_add
- equiv.inhabited'
- order_dual.inhabited
- as_linear_order.inhabited
- units.inhabited
- add_units.inhabited
- monoid.End.inhabited
- add_monoid.End.inhabited
- one_hom.inhabited
- zero_hom.inhabited
- mul_hom.inhabited
- add_hom.inhabited
- monoid_hom.inhabited
- add_monoid_hom.inhabited
- monoid_with_zero_hom.inhabited
- additive.inhabited
- multiplicative.inhabited
- mul_opposite.inhabited
- add_opposite.inhabited
- with_bot.inhabited
- with_top.inhabited
- set.inhabited
- function.End.inhabited
- mul_equiv.inhabited
- add_equiv.inhabited
- with_one.inhabited
- with_zero.inhabited
- rel_embedding.inhabited
- rel_iso.inhabited
- tactic.interactive.mono_cfg.inhabited
- tactic.interactive.mono_selection.inhabited
- order_hom.inhabited
- non_unital_ring_hom.inhabited
- ring_hom.inhabited
- int.inhabited
- pnat.inhabited
- tactic.interactive.rep_arity.inhabited
- pi.lex.inhabited
- multiset.inhabited_multiset
- expr_lens.dir.inhabited
- finset.inhabited_finset
- vector.inhabited
- d_array.inhabited
- array.inhabited
- sym.inhabited_sym
- sym.inhabited_sym'
- ulower.inhabited
- rat.inhabited
- mul_aut.inhabited
- add_aut.inhabited
- tactic.abel.normalize_mode.inhabited
- subsemigroup.inhabited
- add_subsemigroup.inhabited
- submonoid.inhabited
- add_submonoid.inhabited
- set.finite.inhabited
- ring_equiv.inhabited
- free_monoid.inhabited
- free_add_monoid.inhabited
- conj_classes.inhabited
- subgroup.inhabited
- add_subgroup.inhabited
- subsemiring.inhabited
- subring.inhabited
- distrib_mul_action_hom.inhabited
- tactic.ring.normalize_mode.inhabited
- tactic.ring.ring_nf_cfg.inhabited
- linarith.ineq.inhabited
- linarith.comp.inhabited
- linarith.comp_source.inhabited
- prod.lex.inhabited
- pos_num.inhabited
- num.inhabited
- znum.inhabited
- tree.inhabited
- ring_aut.inhabited
- linear_map.inhabited
- sub_mul_action.inhabited
- submodule.inhabited
- associates.inhabited
- submodule.inhabited'
- dfinsupp.inhabited
- finsupp.inhabited
- absolute_value.inhabited
- alist.inhabited
- tactic.tfae.arrow.inhabited
- part.inhabited
- omega_complete_partial_order.chain.inhabited
- omega_complete_partial_order.continuous_hom.inhabited
- alg_equiv.inhabited
- non_unital_alg_hom.inhabited
- con.inhabited
- add_con.inhabited
- con.quotient.inhabited
- add_con.quotient.inhabited
- enat.inhabited
- part_enat.inhabited
- cardinal.inhabited
- linear_pmap.inhabited
- quotient_group.has_quotient.quotient.inhabited
- quotient_add_group.has_quotient.quotient.inhabited
- submodule.quotient.has_quotient.quotient.inhabited
- basis.inhabited
- tensor_product.inhabited
- monoid_algebra.inhabited
- add_monoid_algebra.inhabited
- polynomial.inhabited
- initial_seg.inhabited
- Well_order.inhabited
- ordinal.inhabited
- set_semiring.inhabited
- nat.primes.inhabited_primes
- ideal.quotient.inhabited
- subalgebra.inhabited
- algebra.subalgebra.inhabited
- zmod.inhabited
- cycle.inhabited
- mv_polynomial.inhabited
- localization.inhabited
- add_localization.inhabited
- tactic.ring_exp.coeff.inhabited
- tactic.ring_exp.ex_type.inhabited
- unique_factorization_monoid.normalization_monoid.inhabited
- restrict_scalars.inhabited
- self_adjoint.inhabited
- skew_adjoint.inhabited
- matrix.inhabited
- opposite.inhabited
- prefunctor.inhabited
- category_theory.functor.inhabited
- category_theory.nat_trans.inhabited
- category_theory.iso.inhabited
- category_theory.equivalence.inhabited
- category_theory.adjunction.inhabited
- category_theory.comma.inhabited
- category_theory.comma_morphism.inhabited
- category_theory.arrow.inhabited
- Mon.inhabited
- AddMon.inhabited
- CommMon.inhabited
- AddCommMon.inhabited
- category_theory.End.inhabited
- category_theory.Aut.inhabited
- Group.inhabited
- AddGroup.inhabited
- CommGroup.inhabited
- AddCommGroup.inhabited
- SemiRing.inhabited
- Ring.inhabited
- CommSemiRing.inhabited
- CommRing.inhabited
- local_ring.residue_field.inhabited
- pequiv.inhabited
- composition_as_set.inhabited
- composition.inhabited
- nat.partition.inhabited
- multilinear_map.inhabited
- alternating_map.inhabited
- direct_sum.inhabited
- subfield.inhabited
- adjoin_root.inhabited
- polynomial.splitting_field_aux.inhabited
- polynomial.splitting_field.inhabited
- perfect_closure.inhabited
- lift.subfield_with_hom.inhabited
- unitization.inhabited
- free_algebra.pre.inhabited
- free_algebra.inhabited
- category_theory.discrete.inhabited
- category_theory.limits.inhabited_cone
- category_theory.limits.inhabited_cocone
- category_theory.limits.inhabited_cone_morphism
- category_theory.limits.inhabited_cocone_morphism
- category_theory.ulift_hom.inhabited
- category_theory.as_small.inhabited
- category_theory.limits.walking_parallel_pair.inhabited
- category_theory.limits.walking_parallel_pair_hom.inhabited
- category_theory.limits.wide_pullback_shape.inhabited
- category_theory.limits.wide_pushout_shape.inhabited
- category_theory.limits.wide_pullback_shape.hom.inhabited
- category_theory.limits.wide_pushout_shape.hom.inhabited
- category_theory.Cat.inhabited
- category_theory.skeleton.inhabited
- category_theory.inhabited_thin_skeleton
- category_theory.thin_skeleton.is_skeleton_of_inhabited
- category_theory.over.inhabited
- category_theory.under.inhabited
- category_theory.limits.walking_pair.inhabited
- category_theory.limits.mono_factorisation.inhabited
- category_theory.limits.is_image.inhabited
- category_theory.limits.image_factorisation.inhabited
- category_theory.limits.inhabited_image_map
- category_theory.limits.strong_epi_mono_factorisation_inhabited
- Module.inhabited
- Algebra.inhabited
- category_theory.inhabited_liftable_cone
- category_theory.inhabited_liftable_cocone
- category_theory.inhabited_lifts_to_limit
- category_theory.inhabited_lifts_to_colimit
- category_theory.limits.types.image.inhabited
- category_theory.limits.walking_multicospan.inhabited
- category_theory.limits.walking_multicospan.hom.inhabited
- category_theory.limits.walking_multispan.inhabited
- category_theory.limits.walking_multispan.hom.inhabited
- free_group.inhabited
- abelianization.inhabited
- free_abelian_group.inhabited
- free_ring.inhabited
- free_comm_ring.inhabited
- module.direct_limit.inhabited
- add_comm_group.direct_limit.inhabited
- ring.direct_limit.inhabited
- top_hom.inhabited
- bot_hom.inhabited
- bounded_order_hom.inhabited
- sup_hom.inhabited
- inf_hom.inhabited
- sup_bot_hom.inhabited
- inf_top_hom.inhabited
- lattice_hom.inhabited
- bounded_lattice_hom.inhabited
- as_boolalg.inhabited
- as_boolring.inhabited
- Pointed.inhabited
- Pointed.hom.inhabited
- Bipointed.inhabited
- Bipointed.hom.inhabited
- antisymmetrization.inhabited
- Preorder.inhabited
- PartialOrder.inhabited
- BoundedOrder.inhabited
- Lattice.inhabited
- SemilatticeSup.inhabited
- SemilatticeInf.inhabited
- BoundedLattice.inhabited
- DistribLattice.inhabited
- BoundedDistribLattice.inhabited
- BoolAlg.inhabited
- BoolRing.inhabited
- category_theory.lax_monoidal_functor.inhabited
- category_theory.monoidal_functor.inhabited
- category_theory.free_monoidal_category.inhabited
- hom_rel.inhabited
- category_theory.quotient.inhabited
- category_theory.quotient.hom.inhabited
- quiver.path.inhabited
- category_theory.paths.inhabited
- category_theory.prelax_functor.inhabited
- category_theory.oplax_functor.inhabited
- category_theory.pseudofunctor.inhabited
- category_theory.free_bicategory.inhabited
- category_theory.free_bicategory.hom.inhabited
- category_theory.locally_discrete.inhabited
- category_theory.monoidal_nat_trans.inhabited
- category_theory.lax_braided_functor.inhabited
- category_theory.braided_functor.inhabited
- module.dual.inhabited
- category_theory.is_split_coequalizer.inhabited
- category_theory.mono_over.inhabited
- category_theory.subobject.inhabited
- FinVect.inhabited
- AddCommGroup.colimits.prequotient.inhabited
- AddCommGroup.colimits.colimit_type.inhabited
- GroupWithZero.inhabited
- category_theory.abelian.pseudoelement.inhabited
- Module.colimits.prequotient.inhabited
- Module.colimits.colimit_type.inhabited
- Magma.inhabited
- AddMagma.inhabited
- Semigroup.inhabited
- AddSemigroup.inhabited
- Mon.colimits.prequotient.inhabited
- Mon.colimits.colimit_type.inhabited
- CommRing.colimits.prequotient.inhabited
- CommRing.colimits.colimit_type.inhabited
- lazy_list.inhabited
- stream.inhabited
- computation.inhabited
- seq.inhabited
- seq1.inhabited
- generalized_continued_fraction.pair.inhabited
- generalized_continued_fraction.inhabited
- simple_continued_fraction.inhabited
- continued_fraction.inhabited
- generalized_continued_fraction.int_fract_pair.inhabited
- filter.inhabited_mem
- filter.inhabited
- filter_basis.inhabited
- filter.nat.inhabited_countable_filter_basis
- conj_act.inhabited
- ultrafilter.inhabited
- tactic.decl_reducibility.inhabited
- rel.inhabited
- pfun.inhabited
- inhabited_topological_space
- cofinite_topology.inhabited
- compact_exhaustion.inhabited
- connected_components.inhabited
- separation_quotient.inhabited
- continuous_map.inhabited
- Sup_hom.inhabited
- Inf_hom.inhabited
- frame_hom.inhabited
- complete_lattice_hom.inhabited
- topological_space.opens.inhabited
- topological_space.open_nhds_of.inhabited
- topological_space.closeds.inhabited
- topological_space.clopens.inhabited
- topological_space.compacts.inhabited
- topological_space.nonempty_compacts.inhabited
- topological_space.positive_compacts.inhabited
- topological_space.compact_opens.inhabited
- group_topology.inhabited
- add_group_topology.inhabited
- ring_topology.inhabited
- cubic.inhabited
- graded_monoid.inhabited
- triv_sq_zero_ext.inhabited
- free_magma.inhabited
- free_add_magma.inhabited
- magma.free_semigroup.inhabited
- add_magma.free_add_semigroup.inhabited
- free_semigroup.inhabited
- free_add_semigroup.inhabited
- intermediate_field.inhabited
- intermediate_field.lifts.inhabited
- dmatrix.inhabited
- algebraic_closure.adjoin_monic.inhabited
- algebraic_closure.step.inhabited
- algebraic_closure.inhabited
- cau_seq.inhabited
- cau_seq.completion.Cauchy.inhabited
- real.inhabited
- nonneg.inhabited
- nnreal.inhabited
- ennreal.inhabited
- inhabited_uniform_space
- inhabited_uniform_space_core
- uniform_space.separation_quotient.inhabited
- Cauchy.inhabited
- uniform_space.completion.inhabited
- uniform_space.completion.abstract_completion.inhabited
- complex.inhabited
- group_seminorm.inhabited
- add_group_seminorm.inhabited
- locally_bounded_map.inhabited
- continuous_linear_map.inhabited
- local_equiv.inhabited
- local_equiv.inhabited_of_empty
- affine_map.inhabited
- affine_subspace.inhabited
- linear_isometry.inhabited
- linear_isometry_equiv.inhabited
- affine_isometry.inhabited
- affine_isometry_equiv.inhabited
- closure_operator.inhabited
- lower_adjoint.inhabited
- normed_add_group_hom.inhabited
- unitary.inhabited
- derive_fintype.finset_above.inhabited
- sign_type.inhabited
- real.angle.inhabited
- nat.arithmetic_function.inhabited
- mv_power_series.inhabited
- power_series.inhabited
- hahn_series.inhabited
- hahn_series.summable_family.inhabited
- ratfunc.inhabited
- freiman_hom.inhabited
- add_freiman_hom.inhabited
- category_theory.inhabited_graded_object
- homological_complex.hom.inhabited
- homological_complex.inhabited
- homotopy_equiv.inhabited
- homotopy_category.inhabited
- Top.inhabited
- algebraic_geometry.PresheafedSpace.inhabited
- algebraic_geometry.PresheafedSpace.hom_inhabited
- category_theory.presieve.inhabited
- category_theory.sieve.sieve_inhabited
- category_theory.grothendieck_topology.inhabited
- category_theory.grothendieck_topology.cover.inhabited
- category_theory.pretopology.inhabited
- category_theory.presieve.family_of_elements.inhabited
- category_theory.equalizer.first_obj.inhabited
- category_theory.equalizer.sieve.second_obj.inhabited
- category_theory.equalizer.presieve.second_obj.inhabited
- category_theory.SheafOfTypes.hom.inhabited
- category_theory.SheafOfTypes.inhabited
- category_theory.Sheaf.hom.inhabited
- category_theory.Sheaf.inhabited
- Top.sheaf_inhabited
- category_theory.bicone.inhabited
- category_theory.bicone_hom.inhabited
- category_theory.pairwise.pairwise_inhabited
- category_theory.pairwise.hom_inhabited
- algebraic_geometry.SheafedSpace.inhabited
- topological_space.open_nhds.inhabited
- algebraic_geometry.LocallyRingedSpace.hom.inhabited
- TopCommRing.inhabited
- Top.inhabited_prelocal_predicate
- Top.inhabited_local_predicate
- algebraic_geometry.structure_sheaf.localizations.inhabited
- algebraic_geometry.Scheme.inhabited
- algebraic_geometry.Scheme.open_cover.inhabited
- EllipticCurve.inhabited
- category_theory.morphism_property.inhabited
- algebraic_geometry.affine_target_morphism_property.inhabited
- spectral_map.inhabited
- homogeneous_ideal.inhabited
- LinearOrder.inhabited
- NonemptyFinLinOrd.inhabited
- simplex_category.inhabited
- simplex_category.truncated.inhabited
- category_theory.idempotents.karoubi.hom.inhabited
- category_theory.Groupoid.inhabited
- continuous_map.homotopy.inhabited
- continuous_map.homotopy_with.inhabited
- zeroth_homotopy.inhabited
- path.homotopic.quotient.inhabited
- fundamental_groupoid.inhabited
- fundamental_group.inhabited
- continuous_map.homotopy_equiv.inhabited
- sSet.inhabited
- sSet.truncated.inhabited
- simplicial_object.splitting.index_set.inhabited
- lie_hom.inhabited
- lie_equiv.inhabited
- lie_module_hom.inhabited
- lie_module_equiv.inhabited
- lie_subalgebra.inhabited
- lie_submodule.inhabited
- lie_algebra.commutator_ring.inhabited
- ring_quot.inhabited
- tensor_algebra.inhabited
- universal_enveloping_algebra.inhabited
- free_lie_algebra.inhabited
- lie_submodule.quotient.inhabited
- cartan_matrix.generators.inhabited
- matrix.to_lie_algebra.inhabited
- module.End.eigenvalues.inhabited
- bilin_form.inhabited
- linear_recurrence.inhabited
- fractional_ideal.inhabited
- module.Baer.extension_of.inhabited
- order_monoid_hom.inhabited
- order_add_monoid_hom.inhabited
- order_monoid_with_zero_hom.inhabited
- order_ring_hom.inhabited
- order_ring_iso.inhabited
- shelf_hom.inhabited
- rack.pre_envel_group.inhabited
- rack.pre_envel_group_rel'.inhabited
- rack.envel_group.inhabited
- quaternion_algebra.inhabited
- quaternion.inhabited
- quaternion_algebra.basis.inhabited
- non_unital_star_alg_hom.inhabited
- star_alg_hom.inhabited
- star_subalgebra.inhabited
- sym_alg.inhabited
- tropical.inhabited
- continuous_multilinear_map.inhabited
- formal_multilinear_series.inhabited
- box_integral.box.inhabited
- box_integral.prepartition.inhabited
- box_integral.tagged_prepartition.inhabited
- box_integral.integration_params.inhabited
- box_integral.box_additive_map.inhabited
- measurable_space.inhabited
- measurable_space.dynkin_system.inhabited
- measure_theory.outer_measure.inhabited
- measure_theory.null_measurable_space.inhabited
- list.tprod.inhabited
- measurable_equiv.inhabited
- measure_theory.measure.inhabited
- ereal.inhabited
- urysohns.CU.inhabited
- bounded_continuous_function.inhabited
- measure_theory.simple_func.inhabited
- filter.product.inhabited
- filter.germ.inhabited
- affine.simplex.inhabited
- affine_basis.inhabited
- continuous_linear_map.nonlinear_right_inverse.inhabited
- matrix.special_linear_group.inhabited
- measure_theory.ae_eq_fun.inhabited
- stieltjes_function.inhabited
- continuous_affine_map.inhabited
- convex_cone.inhabited
- weak_dual.inhabited
- normed_space.dual.inhabited
- measure_theory.content.inhabited
- pi_Lp.inhabited
- orthonormal_basis.inhabited
- cont_diff_bump_of_inner.inhabited
- cont_diff_bump.inhabited
- bundle.total_space.inhabited
- bundle.trivial.inhabited
- upper_half_plane.inhabited
- group_filter_basis.inhabited
- add_group_filter_basis.inhabited
- module_filter_basis.inhabited
- seminorm.inhabited
- bump_covering.inhabited
- partition_of_unity.inhabited
- geometry.simplicial_complex.inhabited
- hilbert_basis.inhabited
- ideal.cotangent.inhabited
- derivation.inhabited
- SemiNormedGroup.inhabited
- SemiNormedGroup₁.inhabited
- enorm.inhabited
- picard_lindelof.inhabited
- picard_lindelof.fun_space.inhabited
- measure_theory.vector_measure.inhabited
- measure_theory.jordan_decomposition.inhabited
- besicovitch.satellite_config.inhabited
- besicovitch.ball_package.inhabited
- besicovitch.tau_package.inhabited
- metric.inhabited_left
- metric.inhabited_right
- metric.inductive_limit.inhabited
- semidirect_product.inhabited
- category_theory.action_category.inhabited
- category_theory.limits.walking_parallel_family.inhabited
- category_theory.limits.walking_parallel_family.hom.inhabited
- category_theory.is_kernel_pair.inhabited
- category_theory.monad_hom.inhabited
- category_theory.comonad_hom.inhabited
- category_theory.monad.inhabited
- category_theory.comonad.inhabited
- category_theory.monad.algebra.hom.inhabited
- category_theory.monad.algebra.inhabited
- category_theory.End_monoidal.inhabited
- category_theory.oplax_nat_trans.inhabited
- category_theory.oplax_nat_trans.modification.inhabited
- category_theory.monoidal_single_obj.inhabited
- category_theory.Kleisli.inhabited
- category_theory.Kleisli.mk.inhabited
- PartialFun.inhabited
- category_theory.Quiv.inhabited
- category_theory.Rel.inhabited
- two_pointing.inhabited
- Twop.inhabited
- category_theory.subterminals.inhabited
- category_theory.sigma.sigma_hom.inhabited
- category_theory.connected_components.inhabited
- category_theory.component.inhabited
- category_theory.endofunctor.algebra.inhabited
- category_theory.endofunctor.algebra.hom.inhabited
- category_theory.endofunctor.coalgebra.inhabited
- category_theory.endofunctor.coalgebra.hom.inhabited
- category_theory.enriched_functor.inhabited
- Fintype.inhabited
- Fintype.skeleton.inhabited
- category_theory.grothendieck.hom.inhabited
- category_theory.parallel_pair_inhabited
- category_theory.limits.diagram_of_cones_inhabited
- category_theory.kleisli.inhabited
- category_theory.cokleisli.inhabited
- Mon_.inhabited
- Mon_.hom_inhabited
- CommMon_.inhabited
- Mon_Type_inhabited
- CommMon_Type_inhabited
- Mod.hom_inhabited
- Mod.inhabited
- category_theory.monoidal.transported.inhabited
- category_theory.Mat_.quiver.hom.inhabited
- category_theory.Mat_.inhabited
- category_theory.Mat.inhabited
- category_theory.Mat.quiver.hom.inhabited
- category_theory.triangulated.triangle.inhabited
- category_theory.triangulated.triangle_morphism.inhabited
- category_theory.triangulated.pretriangulated.triangulated_functor_struct.inhabited
- category_theory.triangulated.pretriangulated.triangulated_functor.inhabited
- category_theory.with_terminal.inhabited
- category_theory.with_initial.inhabited
- finset.colex.inhabited
- configuration.dual.inhabited
- combinatorics.line.inhabited
- combinatorics.line.almost_mono.inhabited
- combinatorics.line.color_focused.inhabited
- stone_cech.inhabited
- quiver.wide_subquiver.inhabited
- quiver.labelling.inhabited
- quiver.weakly_connected_component.inhabited
- upper_set.inhabited
- lower_set.inhabited
- simple_graph.inhabited
- simple_graph.subgraph.subgraph_inhabited
- simple_graph.walk.inhabited
- simple_graph.connected_component.inhabited
- finpartition.inhabited
- indexed_partition.inhabited
- indexed_partition.quotient.inhabited
- simple_graph.partition.inhabited
- young_diagram.inhabited
- language.inhabited
- DFA.inhabited
- nzsnum.inhabited
- snum.inhabited
- computability.inhabited_Γ'
- computability.inhabited_fin_encoding
- computability.inhabited_encoding
- NFA.inhabited
- ε_NFA.inhabited
- nat.partrec.code.inhabited
- many_one_degree.inhabited
- regular_expression.inhabited
- turing.list_blank.inhabited
- turing.pointed_map.inhabited
- turing.tape.inhabited
- turing.dir.inhabited
- turing.TM0.stmt.inhabited
- turing.TM0.machine.inhabited
- turing.TM0.cfg.inhabited
- turing.TM1.stmt.inhabited
- turing.TM1.cfg.inhabited
- turing.TM1to0.Λ'.inhabited
- turing.TM1to1.Λ'.inhabited
- turing.TM0to1.Λ'.inhabited
- turing.TM2.stmt.inhabited
- turing.TM2.cfg.inhabited
- turing.TM2to1.Γ'.inhabited
- turing.TM2to1.st_act.inhabited
- turing.TM2to1.Λ'.inhabited
- turing.fin_tm2.σ.inhabited
- turing.fin_tm2.stmt.inhabited
- turing.fin_tm2.inhabited_cfg
- turing.inhabited_fin_tm2
- turing.inhabited_tm2_computable_in_poly_time
- turing.inhabited_tm2_outputs_in_time
- turing.inhabited_tm2_outputs
- turing.inhabited_evals_to_in_time
- turing.inhabited_tm2_evals_to
- turing.inhabited_tm2_computable_in_time
- turing.inhabited_tm2_computable
- turing.inhabited_tm2_computable_aux
- turing.to_partrec.code.inhabited
- turing.to_partrec.cont.inhabited
- turing.to_partrec.cfg.inhabited
- turing.partrec_to_TM2.Γ'.inhabited
- turing.partrec_to_TM2.K'.inhabited
- turing.partrec_to_TM2.cont'.inhabited
- turing.partrec_to_TM2.Λ'.inhabited
- turing.partrec_to_TM2.stmt'.inhabited
- turing.partrec_to_TM2.cfg'.inhabited
- fin2.inhabited
- typevec.inhabited
- typevec.arrow.inhabited
- typevec.last.inhabited
- typevec.curry.inhabited
- buffer.inhabited
- parser.inhabited
- dlist.inhabited
- erased.inhabited
- finmap.inhabited
- semiquot.inhabited
- fp.rmode.inhabited
- fp.float.inhabited
- bucket_array.inhabited
- hash_map.inhabited
- holor.inhabited
- ordnode.inhabited
- ordset.inhabited
- W_type.inhabited
- pfunctor.inhabited
- pfunctor.obj.inhabited
- pfunctor.Idx.inhabited
- mvpfunctor.inhabited
- mvpfunctor.obj.inhabited
- pfunctor.approx.cofix_a.inhabited
- pfunctor.approx.path.inhabited
- pfunctor.M.inhabited
- pfunctor.M_intl.inhabited
- mvpfunctor.M.path.inhabited
- mvpfunctor.inhabited_M
- mvpfunctor.W_path.inhabited
- prime_multiset.inhabited
- pnat.xgcd_type.inhabited
- polynomial_module.inhabited
- mvqpf.cofix.inhabited
- mvqpf.comp.inhabited
- mvqpf.const.inhabited
- mvqpf.prj.inhabited
- mvqpf.quot1.inhabited
- mvqpf.sigma.inhabited
- mvqpf.pi.inhabited
- qpf.cofix.inhabited
- nnrat.inhabited
- hyperreal.inhabited
- wseq.inhabited
- has_finite_inter.inhabited
- vector3.inhabited
- W_type.nat_α.inhabited
- W_type.nat_β.inhabited
- W_type.list_α.inhabited
- W_type.list_β.inhabited
- circle_deg1_lift.inhabited
- flow.inhabited
- galois_field.inhabited
- mv_polynomial.R.inhabited
- open_subgroup.inhabited
- open_add_subgroup.inhabited
- affine.simplex.points_with_circumcenter_index_inhabited
- structure_groupoid.inhabited
- pregroupoid.inhabited
- model_prod_inhabited
- model_pi_inhabited
- topological_vector_bundle_core.inhabited
- basic_smooth_vector_bundle_core.inhabited
- tangent_space.inhabited
- cont_mdiff_map.inhabited
- smooth_monoid_morphism.inhabited
- smooth_add_monoid_morphism.inhabited
- pointed_smooth_map.inhabited
- left_invariant_derivation.inhabited
- smooth_bump_function.inhabited
- locally_constant.inhabited
- euclidean_half_space.inhabited
- euclidean_quadrant.inhabited
- smooth_partition_of_unity.inhabited
- subgroup.left_transversals.inhabited
- add_subgroup.left_transversals.inhabited
- subgroup.right_transversals.inhabited
- add_subgroup.right_transversals.inhabited
- doset.quotient.inhabited
- free_product.inhabited
- free_product.word.inhabited
- free_product.word.pair.inhabited
- sylow.inhabited
- presented_group.inhabited
- subgroup.quotient_diff.inhabited
- dihedral_group.inhabited
- quaternion_group.inhabited
- hamming.inhabited
- quadratic_form.inhabited
- clifford_algebra.inhabited
- clifford_algebra.even_hom.inhabited
- pi_tensor_product.inhabited
- projectivization.subspace.subspace_inhabited
- Meas.inhabited
- measure_theory.finite_measure.inhabited
- measure_theory.probability_measure.inhabited
- first_order.sequence₂.inhabited₀
- first_order.sequence₂.inhabited₁
- first_order.sequence₂.inhabited₂
- first_order.language.inhabited
- first_order.language.hom.inhabited
- first_order.language.embedding.inhabited
- first_order.language.equiv.inhabited
- first_order.language.Lhom.inhabited
- first_order.language.Lequiv.inhabited
- first_order.language.term.inhabited_of_var
- first_order.language.term.inhabited_of_constant
- first_order.language.bounded_formula.inhabited
- first_order.language.substructure.inhabited
- first_order.language.elementary_embedding.inhabited
- first_order.language.elementary_substructure.inhabited
- first_order.language.Theory.Model.inhabited
- first_order.language.definable_set.inhabited
- first_order.language.direct_limit.inhabited
- absolute_value.is_admissible.inhabited
- class_group.inhabited
- function_field.Fqt_infty.inhabited
- cyclotomic_field.inhabited
- cyclotomic_ring.inhabited
- zsqrtd.inhabited
- poly.inhabited
- add_char.inhabited
- mul_char.inhabited
- lucas_lehmer.X.inhabited
- padic.inhabited
- padic_int.inhabited
- CompleteLattice.inhabited
- FinPartialOrder.inhabited
- FinBoolAlg.inhabited
- CompHaus.inhabited
- Frame.inhabited
- ωCPO.inhabited
- concept.inhabited
- order.ideal.inhabited
- order.cofinal.inhabited
- order.partial_iso.inhabited
- linear_extension.inhabited
- heyting.regular.inhabited
- composition_series.inhabited
- order.pfilter.inhabited
- measure_theory.filtration.inhabited
- pmf.inhabited
- Action.inhabited
- Action.hom.inhabited
- representation.as_module.inhabited
- valuation_ring.value_group.inhabited
- valuation_subring.inhabited
- valuation_subring.inhabited_value_group
- is_dedekind_domain.height_one_spectrum.adic_completion.inhabited
- ideal.filtration.inhabited
- ore_localization.inhabited
- perfection.ring.perfection.inhabited
- ring_invo.inhabited
- witt_vector.inhabited
- witt_vector.is_poly.inhabited
- witt_vector.is_poly₂.inhabited
- truncated_witt_vector.inhabited
- pgame.inhabited
- pgame.restricted.inhabited
- pgame.relabelling.inhabited
- game.inhabited
- pgame.inv_ty.inhabited
- nat_ordinal.inhabited
- pgame.domineering.board.inhabited
- lists'.inhabited
- lists.inhabited
- finsets.inhabited
- onote.inhabited
- nonote.inhabited
- surreal.inhabited
- arity.arity.inhabited
- pSet.inhabited
- pSet.type.inhabited
- pSet.resp.inhabited
- Set.inhabited
- Class.inhabited
- omega.term.inhabited
- omega.ee.inhabited
- omega.ee_state.inhabited
- omega.int.preterm.inhabited
- omega.int.preform.inhabited
- omega.nat.preterm.inhabited
- omega.nat.preform.inhabited
- polyrith.poly.inhabited
- polyrith.sage_json_success.inhabited
- polyrith.sage_json_failure.inhabited
- tactic.eliminate.generalization_mode.inhabited
- side.inhabited
- tactic.rewrite_search.side.inhabited
- tactic.rewrite_search.dir_pair.inhabited
- tactic.rewrite_search.using_conv.splice_result.inhabited
- tactic.ring2.csring_expr.inhabited
- tactic.ring2.horner_expr.inhabited
- slim_check.no_shrink.inhabited
- slim_check.small.inhabited
- slim_check.large.inhabited
- slim_check.test_result.inhabited
- slim_check.slim_check_cfg.inhabited
- slim_check.use_has_to_string.inhabited
- slim_check.total_function.inhabited
- slim_check.injective_function.inhabited
- alexandroff.inhabited
- continuous_monoid_hom.inhabited
- continuous_add_monoid_hom.inhabited
- pontryagin_dual.inhabited
- Born.inhabited
- Profinite.inhabited
- Compactum.inhabited
- Locale.inhabited
- discrete_quotient.inhabited
- UniformSpace.inhabited
- CpltSepUniformSpace.inhabited
- cocompact_map.inhabited
- zero_at_infty_continuous_map.inhabited
- continuous_open_map.inhabited
- gen_loop.inhabited
- homotopy_group.inhabited
- Gromov_Hausdorff.GH_space.inhabited
- Gromov_Hausdorff.aux_gluing_struct.inhabited
- continuous_order_hom.inhabited
- pseudo_epimorphism.inhabited
- esakia_hom.inhabited
- clopen_upper_set.inhabited
- Top.presheaf.sheaf_condition.opens_le_cover.inhabited
- compare_reals.Q.inhabited
- compare_reals.Bourbakiℝ.inhabited
- bundle.continuous_linear_map.inhabited
Instances of other typeclasses for inhabited
- inhabited.has_sizeof_inst
@[protected, instance]
Equations
- prop.inhabited = {default := true}
@[protected, instance]
def
pi.inhabited
(α : Sort u)
{β : α → Sort v}
[Π (x : α), inhabited (β x)] :
inhabited (Π (x : α), β x)
Equations
- pi.inhabited α = {default := λ (a : α), inhabited.default}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[class]
- intro : ∀ {α : Sort u}, α → nonempty α
Instances of this typeclass
- has_zero.nonempty
- has_one.nonempty
- has_Inf_to_nonempty
- has_Sup_to_nonempty
- irreducible_space.to_nonempty
- connected_space.to_nonempty
- has_top_nonempty
- has_bot_nonempty
- add_torsor.nonempty
- category_theory.is_connected.is_nonempty
- nontrivial.to_nonempty
- nonempty_of_inhabited
- prod.nonempty
- pi.nonempty
- order_dual.nonempty
- nonempty_lt
- nonempty_gt
- set.univ.nonempty
- set.has_insert.insert.nonempty
- set.image.nonempty
- set.range.nonempty
- set.nonempty_Ici_subtype
- set.nonempty_Iic_subtype
- set.nonempty_Ioi_subtype
- set.nonempty_Iio_subtype
- plift.nonempty
- ulift.nonempty
- finset.has_insert.insert.nonempty
- is_well_order.subtype_nonempty
- cardinal.nonempty_out_aleph
- filter_basis.nonempty_sets
- ultrafilter.nonempty
- separation_quotient.nonempty
- topological_space.nonempty_compacts.to_nonempty
- topological_space.positive_compacts.nonempty'
- Cauchy.nonempty
- affine_map.nonempty
- affine_span.nonempty
- ray_vector.nonempty
- module.ray.nonempty
- category_theory.nonempty_hom_of_connected_groupoid
- category_theory.functor.final.category_theory.structured_arrow.nonempty
- category_theory.functor.initial.category_theory.costructured_arrow.nonempty
- algebraic_geometry.is_integral.nonempty
- nonempty_fin_lin_ord.nonempty
- unit_interval.nonempty
- lie_algebra.commutator_ring.nonempty
- matrix.transvection_struct.nonempty
- affine.simplex.nonempty
- kaehler_differential.nonempty
- category_theory.action_category.nonempty
- two_pointing.nonempty
- category_theory.component.nonempty
- category_theory.grothendieck_topology.subpresheaf.nonempty
- quiver.rooted_connected.nonempty_path
- simple_graph.nonempty_dart_top
- sylow.nonempty
- projectivization.nonempty
- first_order.language.elementary_substructure.nonempty
- first_order.language.Theory.Model.nonempty'
- first_order.language.Theory.Model.nonempty
- first_order.language.ultraproduct.product.nonempty
- Gromov_Hausdorff.rep_GH_space_nonempty
- Top.presheaf.sheaf_condition.category_theory.structured_arrow.nonempty
@[protected]
@[protected, simp, instance]
@[class]
- intro : ∀ {α : Sort u}, (∀ (a b : α), a = b) → subsingleton α
Instances of this typeclass
- is_empty.subsingleton
- unique.subsingleton
- char_p.subsingleton
- subsingleton_prop
- decidable.subsingleton
- pi.subsingleton
- punit.subsingleton
- empty.subsingleton
- subsingleton.prod
- subtype.subsingleton
- subsingleton_pempty
- quot.subsingleton
- quotient.subsingleton
- trunc.subsingleton
- unique.subsingleton_unique
- equiv.equiv_subsingleton_cod
- equiv.equiv_subsingleton_dom
- order_dual.subsingleton
- mul_opposite.subsingleton
- add_opposite.subsingleton
- set.subsingleton_coe_of_subsingleton
- plift.subsingleton
- ulift.subsingleton
- invertible.subsingleton
- ring_hom.int.subsingleton_ring_hom
- fin.order_iso_subsingleton
- fin.order_iso_subsingleton'
- vector.zero_subsingleton
- sym.subsingleton
- fintype.subsingleton
- rat.subsingleton_ring_hom
- subsingleton_rat_module
- nat_algebra_subsingleton
- algebra_rat_subsingleton
- int_algebra_subsingleton
- subsingleton_fin_zero
- subsingleton_fin_one
- locally_finite_order.subsingleton
- locally_finite_order_top.subsingleton
- locally_finite_order_bot.subsingleton
- order.succ_order.subsingleton
- order.pred_order.subsingleton
- initial_seg.subsingleton
- principal_seg.subsingleton
- subalgebra.subsingleton_of_subsingleton
- alg_hom.subsingleton
- alg_equiv.subsingleton_left
- alg_equiv.subsingleton_right
- matrix.subsingleton
- matrix.subsingleton_of_empty_left
- matrix.subsingleton_of_empty_right
- category_theory.subsingleton_of_unop
- category_theory.comm_sq.subsingleton_lift_struct_of_epi
- category_theory.comm_sq.subsingleton_lift_struct_of_mono
- category_theory.discrete.subsingleton
- category_theory.limits.is_limit.subsingleton
- category_theory.limits.is_colimit.subsingleton
- category_theory.limits.preserves_limit_subsingleton
- category_theory.limits.preserves_colimit_subsingleton
- category_theory.limits.preserves_limits_of_shape_subsingleton
- category_theory.limits.preserves_colimits_of_shape_subsingleton
- category_theory.limits.preserves_limits_subsingleton
- category_theory.limits.preserves_colimits_subsingleton
- category_theory.limits.reflects_limit_subsingleton
- category_theory.limits.reflects_colimit_subsingleton
- category_theory.limits.reflects_limits_of_shape_subsingleton
- category_theory.limits.reflects_colimits_of_shape_subsingleton
- category_theory.limits.reflects_limits_subsingleton
- category_theory.limits.reflects_colimits_subsingleton
- category_theory.functor_thin
- category_theory.subsingleton_iso
- category_theory.limits.wide_pullback_shape.subsingleton_hom
- category_theory.limits.wide_pushout_shape.subsingleton_hom
- category_theory.thin_skeleton.thin
- category_theory.limits.walking_cospan.quiver.hom.subsingleton
- category_theory.limits.walking_span.quiver.hom.subsingleton
- category_theory.limits.image_map.subsingleton
- category_theory.limits.has_zero_object.category_theory.iso.subsingleton
- category_theory.limits.has_zero_morphisms.subsingleton
- category_theory.limits.bicone.subsingleton_is_bilimit
- category_theory.subsingleton_preadditive_of_has_binary_biproducts
- category_theory.free_monoidal_category.subsingleton_hom
- category_theory.free_bicategory.locally_thin
- category_theory.mono_over.is_thin
- separation_quotient.subsingleton
- direct_sum.decomposition.subsingleton
- zmod.subsingleton_units
- zmod.subsingleton_ring_hom
- zmod.subsingleton_ring_equiv
- dmatrix.subsingleton
- dmatrix.subsingleton_of_empty_left
- dmatrix.subsingleton_of_empty_right
- zmod.algebra.subsingleton
- hahn_series.subsingleton
- ratfunc.subsingleton
- complex_shape.subsingleton_next
- complex_shape.subsingleton_prev
- continuous_map.subsingleton_subalgebra
- path.subsingleton
- fundamental_groupoid.quiver.hom.subsingleton
- simply_connected_space.path.homotopic.quotient.subsingleton
- lie_subalgebra.subsingleton_of_bot
- lie_submodule.subsingleton_of_bot
- lie_ideal.subsingleton_of_bot
- order_ring_hom.subsingleton
- order_ring_iso.subsingleton_right
- order_ring_iso.subsingleton_left
- sym_alg.subsingleton
- measure_theory.null_measurable_space.subsingleton
- category_theory.is_kernel_pair.subsingleton
- category_theory.subterminals_thin
- category_theory.quiver.hom.subsingleton
- sym2.subsingleton
- typevec.subsingleton0
- pfunctor.approx.cofix_a.subsingleton
- first_order.language.subsingleton_mk₂_functions
- first_order.language.subsingleton_mk₂_relations
- first_order.language.graph.relations.subsingleton
- first_order.language.order.relations.subsingleton
- pgame.subsingleton_short
@[protected]
theorem
subsingleton.helim
{α β : Sort u}
[h : subsingleton α]
(h_1 : α = β)
(a : α)
(b : β) :
a == b
@[protected]
theorem
rec_subsingleton
{p : Prop}
[h : decidable p]
{h₁ : p → Sort u}
{h₂ : ¬p → Sort u}
[h₃ : ∀ (h : p), subsingleton (h₁ h)]
[h₄ : ∀ (h : ¬p), subsingleton (h₂ h)] :
subsingleton (h.rec_on h₂ h₁)
@[protected, instance]
Equations
- ite.decidable = ite.decidable._match_1 d_c
- ite.decidable._match_1 (decidable.is_true hc) = d_t
- ite.decidable._match_1 (decidable.is_false hc) = d_e
@[protected, instance]
def
dite.decidable
{c : Prop}
{t : c → Prop}
{e : ¬c → Prop}
[d_c : decidable c]
[d_t : Π (h : c), decidable (t h)]
[d_e : Π (h : ¬c), decidable (e h)] :
Equations
- dite.decidable = dite.decidable._match_1 d_c
- dite.decidable._match_1 (decidable.is_true hc) = d_t hc
- dite.decidable._match_1 (decidable.is_false hc) = d_e hc
@[ext]
- down : α
Universe lifting operation
Instances for ulift
- ulift.has_sizeof_inst
- ulift.inhabited
- ulift.reflect'
- rel_iso.is_well_order.ulift
- ulift.subsingleton
- ulift.nonempty
- ulift.unique
- ulift.is_empty
- finite.ulift.finite
- ulift.fintype
- ulift.countable
- ulift.encodable
- denumerable.ulift
- ulift.has_one
- ulift.has_zero
- ulift.has_mul
- ulift.has_add
- ulift.has_div
- ulift.has_sub
- ulift.has_inv
- ulift.has_neg
- ulift.has_smul
- ulift.has_vadd
- ulift.has_pow
- ulift.semigroup
- ulift.add_semigroup
- ulift.comm_semigroup
- ulift.add_comm_semigroup
- ulift.mul_one_class
- ulift.add_zero_class
- ulift.mul_zero_one_class
- ulift.monoid
- ulift.add_monoid
- ulift.add_monoid_with_one
- ulift.comm_monoid
- ulift.add_comm_monoid
- ulift.monoid_with_zero
- ulift.comm_monoid_with_zero
- ulift.div_inv_monoid
- ulift.sub_neg_add_monoid
- ulift.group
- ulift.add_group
- ulift.add_group_with_one
- ulift.comm_group
- ulift.add_comm_group
- ulift.group_with_zero
- ulift.comm_group_with_zero
- ulift.left_cancel_semigroup
- ulift.add_left_cancel_semigroup
- ulift.right_cancel_semigroup
- ulift.add_right_cancel_semigroup
- ulift.left_cancel_monoid
- ulift.add_left_cancel_monoid
- ulift.right_cancel_monoid
- ulift.add_right_cancel_monoid
- ulift.cancel_monoid
- ulift.add_cancel_monoid
- ulift.cancel_comm_monoid
- ulift.nontrivial
- ulift.mul_zero_class
- ulift.distrib
- ulift.non_unital_non_assoc_semiring
- ulift.non_assoc_semiring
- ulift.non_unital_semiring
- ulift.semiring
- ulift.non_unital_comm_semiring
- ulift.comm_semiring
- ulift.non_unital_non_assoc_ring
- ulift.non_unital_ring
- ulift.non_assoc_ring
- ulift.ring
- ulift.non_unital_comm_ring
- ulift.comm_ring
- ulift.has_rat_cast
- ulift.field
- ulift.has_smul_left
- ulift.has_vadd_left
- ulift.is_scalar_tower
- ulift.is_scalar_tower'
- ulift.is_scalar_tower''
- ulift.is_central_scalar
- ulift.mul_action
- ulift.add_action
- ulift.mul_action'
- ulift.add_action'
- ulift.distrib_mul_action
- ulift.distrib_mul_action'
- ulift.mul_distrib_mul_action
- ulift.mul_distrib_mul_action'
- ulift.smul_with_zero
- ulift.smul_with_zero'
- ulift.mul_action_with_zero
- ulift.mul_action_with_zero'
- ulift.module
- ulift.module'
- ulift.algebra
- small_ulift
- category_theory.ulift_category
- category_theory.ulift.is_filtered
- category_theory.ulift.is_cofiltered
- ulift.topological_space
- ulift.pseudo_emetric_space
- ulift.emetric_space
- ulift.pseudo_metric_space
- ulift.metric_space
- ulift.seminormed_add_comm_group
- ulift.normed_add_comm_group
- ulift.norm_one_class
- ulift.non_unital_semi_normed_ring
- ulift.semi_normed_ring
- ulift.non_unital_normed_ring
- ulift.normed_ring
- ulift.normed_space
- ulift.normed_algebra
- ulift.nonempty_fin_lin_ord
- ulift.monad
- ulift.is_lawful_functor
- ulift.is_lawful_applicative
- ulift.is_lawful_monad
- slim_check.ulift.sampleable_functor
- down : α
Universe lifting operation from Sort to Type
Instances for plift
Equations
- transitive r = ∀ ⦃x y z : β⦄, r x y → r y z → r x z
Equations
- equivalence r = (reflexive r ∧ symmetric r ∧ transitive r)
theorem
mk_equivalence
{β : Sort v}
(r : β → β → Prop)
(rfl : reflexive r)
(symm : symmetric r)
(trans : transitive r) :
Equations
- irreflexive r = ∀ (x : β), ¬r x x
Equations
- anti_symmetric r = ∀ ⦃x y : β⦄, r x y → r y x → x = y
Equations
- empty_relation = λ (a₁ a₂ : α), false
Instances for empty_relation
Equations
- subrelation q r = ∀ ⦃x y : β⦄, q x y → r x y
Instances for inv_image
theorem
inv_image.trans
{α : Sort u}
{β : Sort v}
(r : β → β → Prop)
(f : α → β)
(h : transitive r) :
transitive (inv_image r f)
theorem
inv_image.irreflexive
{α : Sort u}
{β : Sort v}
(r : β → β → Prop)
(f : α → β)
(h : irreflexive r) :
irreflexive (inv_image r f)
Equations
- commutative f = ∀ (a b : α), f a b = f b a
Equations
- associative f = ∀ (a b c : α), f (f a b) c = f a (f b c)
Equations
- left_identity f one = ∀ (a : α), f one a = a
Equations
- right_identity f one = ∀ (a : α), f a one = a
Equations
- right_inverse f inv one = ∀ (a : α), f a (inv a) = one
Equations
- left_cancelative f = ∀ (a b c : α), f a b = f a c → b = c
Equations
- right_cancelative f = ∀ (a b c : α), f a b = f c b → a = c
Equations
- left_distributive f g = ∀ (a b c : α), f a (g b c) = g (f a b) (f a c)
Equations
- right_distributive f g = ∀ (a b c : α), f (g a b) c = g (f a c) (f b c)
Equations
- right_commutative h = ∀ (b : β) (a₁ a₂ : α), h (h b a₁) a₂ = h (h b a₂) a₁
Equations
- left_commutative h = ∀ (a₁ a₂ : α) (b : β), h a₁ (h a₂ b) = h a₂ (h a₁ b)
theorem
right_comm
{α : Type u}
(f : α → α → α) :
commutative f → associative f → right_commutative f