Documentation Verification Report

Irrational

📁 Source: Mathlib/Topology/Instances/Irrational.lean

Statistics

MetricCount
DefinitionsIrrational
1
Theoremseventually_forall_le_dist_cast_div, eventually_forall_le_dist_cast_div_of_denom_le, eventually_forall_le_dist_cast_rat_of_den_le, instDenselyOrderedSubtypeReal, instNoMaxOrderSubtypeReal, instNoMinOrderSubtypeReal, instOrderTopologySubtypeReal, setOf_irrational, dense_irrational, eventually_residual_irrational
10
Total11

Irrational

Theorems

NameKindAssumesProvesValidatesDepends On
eventually_forall_le_dist_cast_div 📖mathematicalIrrationalFilter.Eventually
Real
nhds
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
Real.pseudoMetricSpace
Real.instZero
IsClosedMap.isClosed_range
IsClosedMap.comp
isClosedMap_smul₀
T5Space.toT1Space
OrderTopology.t5Space
instOrderTopologyReal
SeparatelyContinuousMul.to_continuousSMul
IsSemitopologicalSemiring.toSeparatelyContinuousMul
IsSemitopologicalRing.toIsSemitopologicalSemiring
IsTopologicalRing.toIsSemitopologicalRing
instIsTopologicalRingReal
Topology.IsClosedEmbedding.isClosedMap
Int.isClosedEmbedding_coe_real
Metric.mem_nhds_iff
IsOpen.mem_nhds
IsClosed.isOpen_compl
Filter.Eventually.mono
ge_mem_nhds
not_lt
Metric.ball_subset_ball
dist_comm
div_eq_inv_mul
eventually_forall_le_dist_cast_div_of_denom_le 📖mathematicalIrrationalFilter.Eventually
Real
nhds
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
Real.pseudoMetricSpace
Real.instZero
Set.Finite.eventually_all
Set.finite_le_nat
eventually_forall_le_dist_cast_div
eventually_forall_le_dist_cast_rat_of_den_le 📖mathematicalIrrationalFilter.Eventually
Real
nhds
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
Real.pseudoMetricSpace
Real.instZero
Filter.Eventually.mono
eventually_forall_le_dist_cast_div_of_denom_le
Rat.cast_def
instDenselyOrderedSubtypeReal 📖mathematicalDenselyOrdered
Real
Irrational
Real.instLT
exists_irrational_btwn
instNoMaxOrderSubtypeReal 📖mathematicalNoMaxOrder
Real
Irrational
Real.instLT
add_natCast
Nat.cast_one
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
instIsLeftCancelAddOfAddLeftReflectLE
IsOrderedCancelAddMonoid.toAddLeftReflectLE
Real.instIsOrderedCancelAddMonoid
IsOrderedAddMonoid.toAddLeftMono
Real.instIsOrderedAddMonoid
contravariant_lt_of_covariant_le
Real.instZeroLEOneClass
NeZero.charZero_one
IsStrictOrderedRing.toCharZero
Real.instIsStrictOrderedRing
instNoMinOrderSubtypeReal 📖mathematicalNoMinOrder
Real
Irrational
Real.instLT
sub_natCast
Nat.cast_one
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
instIsLeftCancelAddOfAddLeftReflectLE
IsOrderedCancelAddMonoid.toAddLeftReflectLE
Real.instIsOrderedCancelAddMonoid
IsOrderedAddMonoid.toAddLeftMono
Real.instIsOrderedAddMonoid
Real.instZeroLEOneClass
NeZero.charZero_one
IsStrictOrderedRing.toCharZero
Real.instIsStrictOrderedRing
instOrderTopologySubtypeReal 📖mathematicalOrderTopology
Real
Irrational
instTopologicalSpaceSubtype
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
Real.pseudoMetricSpace
Subtype.preorder
Real.instPreorder
induced_orderTopology
instOrderTopologyReal
exists_irrational_btwn

IsGδ

Theorems

NameKindAssumesProvesValidatesDepends On
setOf_irrational 📖mathematicalIsGδ
Real
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
Real.pseudoMetricSpace
setOf
Irrational
Set.Countable.isGδ_compl
T5Space.toT1Space
OrderTopology.t5Space
instOrderTopologyReal
Set.countable_range
Encodable.countable

(root)

Definitions

NameCategoryTheorems
Irrational 📖MathDef
123 mathmath: Irrational.instNoMaxOrderSubtypeReal, Real.goldenConj_irrational, eventually_residual_irrational, Irrational.ratCast_sub, Transcendental.irrational, Irrational.of_intCast_div, Irrational.ratCast_mul, Irrational.of_natCast_add, Irrational.of_ratCast_sub, Irrational.of_intCast_sub, Irrational.of_natCast_sub, Irrational.of_div_natCast, Irrational.ratCast_div, Irrational.div_cases, irrational_sqrt_ratCast_iff, Irrational.natCast_add, irrational_sqrt_intCast_iff, Irrational.intCast_add, irrational_mul_natCast_iff, Irrational.mul_intCast, Irrational.intCast_mul, Real.goldenRatio_irrational, Irrational.of_pow, Irrational.of_zpow, Irrational.of_one_div, Irrational.neg, Irrational.add_cases, irrational_intCast_sub_iff, Irrational.of_natCast_mul, Irrational.of_neg, Irrational.mul_natCast, irrational_sqrt_natCast_iff, irrational_sqrt_ratCast_iff_of_nonneg, Irrational.of_sub_ratCast, Irrational.add_natCast, Irrational.inv, irrational_ratCast_mul_iff, Irrational.instOrderTopologySubtypeReal, Irrational.intCast_div, not_irrational_zero, irrational_mul_ratCast_iff, dense_irrational, irrational_mul_intCast_iff, irrational_natCast_mul_iff, irrational_div_natCast_iff, irrational_nrt_of_notint_nrt, irrational_sqrt_intCast_iff_of_nonneg, Irrational.of_intCast_mul, Irrational.sub_ratCast, Liouville.irrational, Irrational.div_intCast, irrational_div_intCast_iff, Irrational.of_ratCast_mul, Polynomial.Chebyshev.irrational_of_isRoot_T_real, IsGδ.setOf_irrational, Irrational.natCast_sub, Irrational.of_ratCast_div, Irrational.of_mul_natCast, irrational_inv_iff, Irrational.natCast_div, Irrational.of_mul_ratCast, irrational_add_intCast_iff, Irrational.natCast_mul, irrational_iff_ne_rational, Irrational.sub_intCast, not_irrational_ofNat, irrational_sqrt_of_multiplicity_odd, Irrational.instDenselyOrderedSubtypeReal, irrational_ratCast_div_iff, irrational_natCast_sub_iff, irrational_pi, irrational_ratCast_add_iff, Irrational.ratCast_add, irrational_sub_intCast_iff, irrational_sub_ratCast_iff, AddCircle.denseRange_zsmul_coe_iff, irrational_div_ratCast_iff, Irrational.instNoMinOrderSubtypeReal, irrational_ratCast_sub_iff, Irrational.of_natCast_div, Rat.not_irrational, Irrational.of_add_intCast, irrational_add_natCast_iff, Int.not_irrational, Irrational.add_ratCast, dense_addSubgroupClosure_pair_iff, Irrational.sub_natCast, Irrational.of_mul_self, LiouvilleWith.irrational, Irrational.intCast_sub, Irrational.of_inv, not_irrational_one, Irrational.of_add_natCast, Irrational.mul_cases, Irrational.of_sub_intCast, exists_irrational_btwn, Irrational.add_intCast, Irrational.div_natCast, irrational_nrt_of_n_not_dvd_multiplicity, Irrational.div_ratCast, Irrational.mul_ratCast, irrational_cos_rat_mul_pi, irrational_sub_natCast_iff, irrational_neg_iff, Irrational.of_div_ratCast, irrational_add_ratCast_iff, setOf_liouville_eq_irrational_inter_iInter_iUnion, Nat.not_irrational, Irrational.of_add_ratCast, irrational_intCast_add_iff, Irrational.of_intCast_add, irrational_sqrt_ofNat_iff, irrational_intCast_div_iff, Nat.Prime.irrational_sqrt, irrational_natCast_add_iff, Irrational.of_ratCast_add, Irrational.of_mul_intCast, irrational_natCast_div_iff, irrational_sqrt_two, Irrational.of_sub_natCast, Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational, Irrational.of_div_intCast, irrational_intCast_mul_iff

Theorems

NameKindAssumesProvesValidatesDepends On
dense_irrational 📖mathematicalDense
Real
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
Real.pseudoMetricSpace
setOf
Irrational
TopologicalSpace.IsTopologicalBasis.dense_iff
Real.isTopologicalBasis_Ioo_rat
Set.inter_comm
exists_irrational_btwn
Rat.cast_lt
Real.instIsStrictOrderedRing
eventually_residual_irrational 📖mathematicalFilter.Eventually
Real
Irrational
residual
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
Real.pseudoMetricSpace
residual_of_dense_Gδ
IsGδ.setOf_irrational
dense_irrational

---

← Back to Index